--- a/src/Tools/Code/code_preproc.ML Fri Sep 06 15:47:51 2013 +0200
+++ b/src/Tools/Code/code_preproc.ML Fri Sep 06 20:55:14 2013 +0200
@@ -143,7 +143,7 @@
val resubst = curry (Term.betapplys o swap) all_vars;
in (resubst, term_of_conv thy conv (fold_rev lambda all_vars t)) end;
-fun lift_ss_conv f ss ct = f (Simplifier.put_simpset ss (Proof_Context.init_global (theory_of_cterm ct))) ct;
+fun lift_ss_conv f ss ct = f (Simplifier.global_context (theory_of_cterm ct) ss) ct;
fun preprocess_conv thy =
let
--- a/src/Tools/Code/code_simp.ML Fri Sep 06 15:47:51 2013 +0200
+++ b/src/Tools/Code/code_simp.ML Fri Sep 06 20:55:14 2013 +0200
@@ -63,7 +63,7 @@
simpset_map (Proof_Context.init_global thy) (add_program program) (simpset_default thy some_ss);
fun lift_ss_conv f ss ct =
- f (Proof_Context.init_global (theory_of_cterm ct) |> Simplifier.put_simpset ss |> set_trace) ct;
+ f (Simplifier.global_context (theory_of_cterm ct) ss |> set_trace) ct;
fun rewrite_modulo thy some_ss program =
lift_ss_conv Simplifier.full_rewrite (simpset_program thy some_ss program);