# HG changeset patch
# User haftmann
# Date 1378493714 -7200
# Node ID b098d53152d98f717f45b5e02c8d664b59966c00
# Parent  ef2bb63583aca8165fdf9f8710f8a020889829f2
tuned

diff -r ef2bb63583ac -r b098d53152d9 src/Tools/Code/code_preproc.ML
--- 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
diff -r ef2bb63583ac -r b098d53152d9 src/Tools/Code/code_simp.ML
--- 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);