--- a/src/Tools/Code/code_preproc.ML Mon May 03 07:59:51 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML Mon May 03 14:25:56 2010 +0200
@@ -87,7 +87,7 @@
fun add_unfold_post raw_thm thy =
let
- val thm = Local_Defs.meta_rewrite_rule (ProofContext.init thy) raw_thm;
+ val thm = Local_Defs.meta_rewrite_rule (ProofContext.init_global thy) raw_thm;
val thm_sym = Thm.symmetric thm;
in
thy |> map_pre_post (fn (pre, post) =>
@@ -157,7 +157,7 @@
fun print_codeproc thy =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val pre = (#pre o the_thmproc) thy;
val post = (#post o the_thmproc) thy;
val functrans = (map fst o #functrans o the_thmproc) thy;