Fix machine-code compiler code in face of thm rebinding restrictions

Fix is to explicitly allow rebinds when this code makes its
definitions and does its theorem-saving.

examples/machine-code/decompiler/decompilerLib.sml

@@ -12,7 +12,11 @@ struct
    val (Type, Term) = parse_from_grammars addressTheory.address_grammars
 end
 
-val new_definition = Definition.new_definition (* not boolSyntax! *)
+fun allow_rebinds f x = Feedback.trace ("Theory.allow_rebinds", 1) f x
+val new_definition =
+    allow_rebinds Definition.new_definition (* not boolSyntax! *)
+val save_thm = allow_rebinds save_thm
+
 
 (* -------------------------------------------------------------------------- *)
 (* Decompilation stages:                                                      *)

examples/machine-code/hoare-triple/tailrecLib.sml

@@ -11,6 +11,9 @@ struct
 end
 
 val tailrec_definitions = ref ([]:thm list);
+fun allow_rebinds f x = Feedback.trace ("Theory.allow_rebinds", 1) f x
+val new_definition = allow_rebinds new_definition
+val save_thm = allow_rebinds save_thm
 
 (* tactic, move to helperLib? *)