# HG changeset patch
# User haftmann
# Date 1388783084 -3600
# Node ID f1ded3cea58de780d4353bb5c446423038c24cf0
# Parent  cb077b02c9a43a718e9daa1b52d9c95497927a81
proper context for simplifier invocations in code generation stack

diff -r cb077b02c9a4 -r f1ded3cea58d src/Tools/Code/code_preproc.ML
--- 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);
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 *)