| 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) =>