more correct context for dynamic invocations of static code conversions etc.

--- a/src/Tools/Code/code_preproc.ML	Sat Jul 27 16:59:25 2013 +0200
+++ b/src/Tools/Code/code_preproc.ML	Sat Jul 27 18:02:41 2013 +0200
@@ -143,11 +143,13 @@
     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 = f (Simplifier.put_simpset ss (Proof_Context.init_global (theory_of_cterm ct))) ct;
+
 fun preprocess_conv thy =
   let
-    val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
+    val pre = (#pre o the_thmproc) thy;
   in
-    Simplifier.rewrite pre
+    lift_ss_conv Simplifier.rewrite pre
     #> trans_conv_rule (Axclass.unoverload_conv thy)
   end;
 
@@ -155,10 +157,10 @@
 
 fun postprocess_conv thy =
   let
-    val post = (Simplifier.global_context thy o #post o the_thmproc) thy;
+    val post = (#post o the_thmproc) thy;
   in
     Axclass.overload_conv thy
-    #> trans_conv_rule (Simplifier.rewrite post)
+    #> trans_conv_rule (lift_ss_conv Simplifier.rewrite post)
   end;
 
 fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);
@@ -484,11 +486,12 @@
   let
     val (algebra, eqngr) = obtain true thy consts [];
     val evaluator' = evaluator algebra eqngr;
+    val postproc' = postprocess_term thy;
   in 
     preprocess_term thy
     #-> (fn resubst => fn t => t
       |> evaluator' (Term.add_tfrees t [])
-      |> postproc (postprocess_term thy o resubst))
+      |> postproc (postproc' o resubst))
   end;
 
 

--- a/src/Tools/Code/code_simp.ML	Sat Jul 27 16:59:25 2013 +0200
+++ b/src/Tools/Code/code_simp.ML	Sat Jul 27 18:02:41 2013 +0200
@@ -11,7 +11,7 @@
   val dynamic_tac: theory -> int -> tactic
   val dynamic_value: theory -> term -> term
   val static_conv: theory -> simpset option -> string list -> conv
-  val static_tac: theory -> simpset option -> string list -> int -> tactic
+  val static_tac: theory -> simpset option -> string list -> Proof.context -> int -> tactic
   val setup: theory -> theory
 end;
 
@@ -30,24 +30,34 @@
 
 fun map_ss f thy = Simpset.map (simpset_map (Proof_Context.init_global thy) f) thy;
 
-fun simpset_default thy = Simplifier.global_context thy o the_default (Simpset.get thy);
+fun simpset_default thy = the_default (Simpset.get thy);
 
 
 (* build simpset and conversion from program *)
 
 fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
-      ss addsimps (map_filter (fst o snd)) eqs
+      ss
+      |> fold Simplifier.add_simp ((map_filter (fst o snd)) eqs)
       |> fold Simplifier.add_cong (the_list some_cong)
   | add_stmt (Code_Thingol.Classinst { inst_params, ... }) ss =
-      ss addsimps (map (fst o snd) inst_params)
+      ss
+      |> 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 rewrite_modulo thy some_ss program = Simplifier.full_rewrite
-  (add_program program (simpset_default thy some_ss));
+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.put_simpset ss (Proof_Context.init_global (theory_of_cterm ct))) ct;
 
-fun conclude_tac thy some_ss = Simplifier.full_simp_tac (simpset_default thy some_ss);
+fun rewrite_modulo thy some_ss program =
+  lift_ss_conv Simplifier.full_rewrite (simpset_program thy some_ss program);
+
+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;
 
 
 (* evaluation with dynamic code context *)
@@ -55,7 +65,7 @@
 fun dynamic_conv thy = Code_Thingol.dynamic_conv thy
   (fn _ => fn program => fn _ => fn _ => rewrite_modulo thy NONE program);
 
-fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE;
+fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE (Proof_Context.init_global thy);
 
 fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy;
 
@@ -72,7 +82,10 @@
   Code_Thingol.static_conv_simple thy consts
     (fn program => fn _ => fn _ => rewrite_modulo thy some_ss program);
 
-fun static_tac thy some_ss consts = CONVERSION (static_conv thy some_ss consts)
-  THEN' conclude_tac thy some_ss;
+fun static_tac thy some_ss consts =
+  let
+    val conv = static_conv thy some_ss consts;
+    val tac = conclude_tac thy some_ss;
+  in fn ctxt => CONVERSION conv THEN' tac ctxt end;
 
 end;