diff -r cb077b02c9a4 -r f1ded3cea58d src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Fri Jan 03 21:52:00 2014 +0100
+++ b/src/Tools/Code/code_simp.ML	Fri Jan 03 22:04:44 2014 +0100
@@ -31,7 +31,11 @@
 
 fun map_ss f thy = Simpset.map (simpset_map (Proof_Context.init_global thy) f) thy;
 
-fun simpset_default thy = the_default (Simpset.get thy);
+fun simpset_default thy some_ss = the_default (Simpset.get thy) some_ss;
+
+fun simp_ctxt_default thy some_ss =
+  Proof_Context.init_global thy
+  |> put_simpset (simpset_default thy some_ss);
 
 
 (* diagnostic *)
@@ -59,19 +63,15 @@
 
 val add_program = Graph.fold (add_stmt o fst o snd);
 
-fun simpset_program thy some_ss program =
-  simpset_map (Proof_Context.init_global thy) (add_program program) (simpset_default thy some_ss);
-
-fun lift_ss_conv f ss ct =  (* FIXME proper context!? *)
-  f (Proof_Context.init_global (theory_of_cterm ct) |> put_simpset ss |> set_trace) ct;
+fun simp_ctxt_program thy some_ss program =
+  simp_ctxt_default thy some_ss
+  |> add_program program;
 
 fun rewrite_modulo thy some_ss program =
-  lift_ss_conv Simplifier.full_rewrite (simpset_program thy some_ss program);
+  Simplifier.full_rewrite (simp_ctxt_program thy some_ss program |> set_trace);
 
 fun conclude_tac thy some_ss =
-  let
-    val ss = simpset_default thy some_ss;
-  in fn ctxt => Simplifier.full_simp_tac (Simplifier.put_simpset ss ctxt) end;
+  Simplifier.full_simp_tac o Simplifier.put_simpset (simpset_default thy some_ss);
 
 
 (* evaluation with dynamic code context *)