src/Tools/Code/code_preproc.ML
changeset 35624 c4e29a0bb8c1
parent 35235 7c7cfe69d7f6
child 36102 a51d1d154c71
--- a/src/Tools/Code/code_preproc.ML	Sat Mar 06 19:17:59 2010 +0000
+++ b/src/Tools/Code/code_preproc.ML	Sun Mar 07 11:57:16 2010 +0100
@@ -87,7 +87,7 @@
 
 fun add_unfold_post raw_thm thy =
   let
-    val thm = LocalDefs.meta_rewrite_rule (ProofContext.init thy) raw_thm;
+    val thm = Local_Defs.meta_rewrite_rule (ProofContext.init thy) raw_thm;
     val thm_sym = Thm.symmetric thm;
   in
     thy |> map_pre_post (fn (pre, post) =>