--- a/src/Tools/Code/code_simp.ML Wed Jan 01 13:24:23 2014 +0100
+++ b/src/Tools/Code/code_simp.ML Wed Jan 01 14:29:22 2014 +0100
@@ -62,8 +62,8 @@
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 =
- f (Simplifier.global_context (theory_of_cterm ct) ss |> set_trace) ct;
+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 rewrite_modulo thy some_ss program =
lift_ss_conv Simplifier.full_rewrite (simpset_program thy some_ss program);