src/Tools/Code/code_simp.ML

   val merge = merge_ss;
 );
 
 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 *)
 
 val trace = Attrib.setup_config_bool @{binding "code_simp_trace"} (K false);

       |> fold Simplifier.add_simp (map (fst o snd) inst_params)
   | add_stmt _ ss = ss;
 
 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 *)
 
 fun dynamic_conv thy = Code_Thingol.dynamic_conv thy