Fix a reference to tailrecLib that a1129a6 didn't catch

HOL-Theorem-Prover · Nov 29, 2023 · 24dd865 · 24dd865
1 parent 6d57be5
commit 24dd865
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/examples/machine-code/multiword/mc_multiwordScript.sml b/examples/machine-code/multiword/mc_multiwordScript.sml
@@ -11,7 +11,7 @@ val _ = temp_delsimps ["NORMEQ_CONV"]
 val REV = Tactical.REVERSE;
 
 fun tailrec_define name tm = let
-  val (def,t1,pre,t2) = tailrecLib.tailrec_define_from_step name tm NONE;
+  val (def,t1,pre,t2) = mc_tailrecLib.tailrec_define_from_step name tm NONE;
   val _ = save_thm(name ^ "_def", def)
   val _ = save_thm(name ^ "_pre_def", pre)
   in (def,t1,pre,t2) end