--- a/src/Tools/Code/code_preproc.ML Fri Jan 03 21:52:00 2014 +0100
+++ b/src/Tools/Code/code_preproc.ML Fri Jan 03 22:04:44 2014 +0100
@@ -143,14 +143,15 @@
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 = (* FIXME proper context!? *)
- f (Proof_Context.init_global (theory_of_cterm ct) |> put_simpset ss) ct;
+fun global_simpset_context thy ss =
+ Proof_Context.init_global thy
+ |> put_simpset ss;
fun preprocess_conv thy =
let
- val pre = (#pre o the_thmproc) thy;
+ val pre = global_simpset_context thy ((#pre o the_thmproc) thy);
in
- lift_ss_conv Simplifier.rewrite pre
+ Simplifier.rewrite pre
#> trans_conv_rule (Axclass.unoverload_conv thy)
end;
@@ -158,10 +159,10 @@
fun postprocess_conv thy =
let
- val post = (#post o the_thmproc) thy;
+ val post = global_simpset_context thy ((#post o the_thmproc) thy);
in
Axclass.overload_conv thy
- #> trans_conv_rule (lift_ss_conv Simplifier.rewrite post)
+ #> trans_conv_rule (Simplifier.rewrite post)
end;
fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);
--- 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 *)