build up preprocessing context only once

--- a/src/Pure/Isar/code.ML	Sun Feb 09 15:26:33 2014 +0100
+++ b/src/Pure/Isar/code.ML	Sun Feb 09 15:26:33 2014 +0100
@@ -727,8 +727,9 @@
   | Abstract of thm * string
 with
 
-fun dummy_thm thy c =
+fun dummy_thm ctxt c =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val raw_ty = devarify (const_typ thy c);
     val (vs, _) = typscheme thy (c, raw_ty);
     val sortargs = case Axclass.class_of_param thy c
@@ -742,11 +743,12 @@
     val chead = build_head thy (c, ty);
   in Thm.weaken chead Drule.dummy_thm end;
 
-fun nothing_cert thy c = Nothing (dummy_thm thy c);
+fun nothing_cert ctxt c = Nothing (dummy_thm ctxt c);
 
-fun cert_of_eqns thy c [] = Equations (dummy_thm thy c, [])
-  | cert_of_eqns thy c raw_eqns = 
+fun cert_of_eqns ctxt c [] = Equations (dummy_thm ctxt c, [])
+  | cert_of_eqns ctxt c raw_eqns = 
       let
+        val thy = Proof_Context.theory_of ctxt;
         val eqns = burrow_fst (canonize_thms thy) raw_eqns;
         val _ = map (assert_eqn thy) eqns;
         val (thms, propers) = split_list eqns;
@@ -900,33 +902,38 @@
       else Conv.all_conv ct;
   in Conv.combination_conv (Conv.arg_conv lhs_conv) conv ct end;
 
-fun rewrite_eqn thy conv ss =
-  let
-    val ctxt = Proof_Context.init_global thy;
-    val rewrite = Conv.fconv_rule (conv (Simplifier.rewrite (put_simpset ss ctxt)));
-  in singleton (Variable.trade (K (map rewrite)) ctxt) end;
+fun rewrite_eqn conv ctxt =
+  singleton (Variable.trade (K (map (Conv.fconv_rule (conv (Simplifier.rewrite ctxt))))) ctxt)
 
-fun preprocess thy conv ss =
-  Thm.transfer thy
-  #> rewrite_eqn thy conv ss
-  #> Axclass.unoverload thy
+fun preprocess conv ctxt =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+  in
+    Thm.transfer thy
+    #> rewrite_eqn conv ctxt
+    #> Axclass.unoverload thy
+  end;
 
-fun cert_of_eqns_preprocess thy functrans ss c =
+fun cert_of_eqns_preprocess ctxt functrans c =
   perhaps (perhaps_loop (perhaps_apply functrans))
-  #> (map o apfst) (preprocess thy eqn_conv ss)
-  #> cert_of_eqns thy c;
+  #> (map o apfst) (preprocess eqn_conv ctxt)
+  #> cert_of_eqns ctxt c;
 
 fun get_cert thy { functrans, ss } c =
-  case retrieve_raw thy c
-   of Default (eqns, eqns_lazy) => Lazy.force eqns_lazy
-        |> cert_of_eqns_preprocess thy functrans ss c
+  let
+    val ctxt = thy |> Proof_Context.init_global |> put_simpset ss;
+  in
+    case retrieve_raw thy c of
+      Default (_, eqns_lazy) => Lazy.force eqns_lazy
+        |> cert_of_eqns_preprocess ctxt functrans c
     | Eqns eqns => eqns
-        |> cert_of_eqns_preprocess thy functrans ss c
-    | None => nothing_cert thy c
+        |> cert_of_eqns_preprocess ctxt functrans c
+    | None => nothing_cert ctxt c
     | Proj (_, tyco) => cert_of_proj thy c tyco
     | Abstr (abs_thm, tyco) => abs_thm
-        |> preprocess thy Conv.arg_conv ss
-        |> cert_of_abs thy tyco c;
+       |> preprocess Conv.arg_conv ctxt
+       |> cert_of_abs thy tyco c
+  end;
 
 
 (* cases *)

--- a/src/Tools/Code/code_preproc.ML	Sun Feb 09 15:26:33 2014 +0100
+++ b/src/Tools/Code/code_preproc.ML	Sun Feb 09 15:26:33 2014 +0100
@@ -264,15 +264,16 @@
 
 (* retrieving equations and instances from the background context *)
 
-fun obtain_eqns thy eqngr c =
+fun obtain_eqns ctxt eqngr c =
   case try (Graph.get_node eqngr) c
    of SOME (lhs, cert) => ((lhs, []), cert)
     | NONE => let
+        val thy = Proof_Context.theory_of ctxt;
         val functrans = (map (fn (_, (_, f)) => f thy)
           o #functrans o the_thmproc) thy;
-        val {pre, ...} = the_thmproc thy;
-        val cert = Code.get_cert thy { functrans = functrans, ss = pre } c;
-        val (lhs, rhss) = Code.typargs_deps_of_cert thy cert;
+        val cert = Code.get_cert thy { functrans = functrans, ss = simpset_of ctxt } c; (*FIXME*)
+        val (lhs, rhss) =
+          Code.typargs_deps_of_cert thy cert;
       in ((lhs, rhss), cert) end;
 
 fun obtain_instance thy arities (inst as (class, tyco)) =
@@ -289,7 +290,7 @@
 
 (* computing instantiations *)
 
-fun add_classes thy arities eqngr c_k new_classes vardeps_data =
+fun add_classes ctxt arities eqngr c_k new_classes vardeps_data =
   let
     val (styps, old_classes) = Vargraph.get_node (fst vardeps_data) c_k;
     val diff_classes = new_classes |> subtract (op =) old_classes;
@@ -299,82 +300,82 @@
   in
     vardeps_data
     |> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes)
-    |> fold (fn styp => fold (ensure_typmatch_inst thy arities eqngr styp) new_classes) styps
-    |> fold (fn c_k => add_classes thy arities eqngr c_k diff_classes) c_ks
+    |> fold (fn styp => fold (ensure_typmatch_inst ctxt arities eqngr styp) new_classes) styps
+    |> fold (fn c_k => add_classes ctxt arities eqngr c_k diff_classes) c_ks
   end end
-and add_styp thy arities eqngr c_k new_tyco_styps vardeps_data =
+and add_styp ctxt arities eqngr c_k new_tyco_styps vardeps_data =
   let
     val (old_tyco_stypss, classes) = Vargraph.get_node (fst vardeps_data) c_k;
   in if member (op =) old_tyco_stypss new_tyco_styps then vardeps_data
   else
     vardeps_data
     |> (apfst o Vargraph.map_node c_k o apfst) (cons new_tyco_styps)
-    |> fold (ensure_typmatch_inst thy arities eqngr new_tyco_styps) classes
+    |> fold (ensure_typmatch_inst ctxt arities eqngr new_tyco_styps) classes
   end
-and add_dep thy arities eqngr c_k c_k' vardeps_data =
+and add_dep ctxt arities eqngr c_k c_k' vardeps_data =
   let
     val (_, classes) = Vargraph.get_node (fst vardeps_data) c_k;
   in
     vardeps_data
-    |> add_classes thy arities eqngr c_k' classes
+    |> add_classes ctxt arities eqngr c_k' classes
     |> apfst (Vargraph.add_edge (c_k, c_k'))
   end
-and ensure_typmatch_inst thy arities eqngr (tyco, styps) class vardeps_data =
-  if can (Sign.arity_sorts thy tyco) [class]
+and ensure_typmatch_inst ctxt arities eqngr (tyco, styps) class vardeps_data =
+  if can (Sign.arity_sorts (Proof_Context.theory_of ctxt) tyco) [class]
   then vardeps_data
-    |> ensure_inst thy arities eqngr (class, tyco)
+    |> ensure_inst ctxt arities eqngr (class, tyco)
     |> fold_index (fn (k, styp) =>
-         ensure_typmatch thy arities eqngr styp (Inst (class, tyco), k)) styps
+         ensure_typmatch ctxt arities eqngr styp (Inst (class, tyco), k)) styps
   else vardeps_data (*permissive!*)
-and ensure_inst thy arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) =
+and ensure_inst ctxt arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) =
   if member (op =) insts inst then vardeps_data
   else let
     val (classess, (super_classes, inst_params)) =
-      obtain_instance thy arities inst;
+      obtain_instance (Proof_Context.theory_of ctxt) arities inst;
   in
     vardeps_data
     |> (apsnd o apsnd) (insert (op =) inst)
     |> fold_index (fn (k, _) =>
          apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))) classess
-    |> fold (fn super_class => ensure_inst thy arities eqngr (super_class, tyco)) super_classes
-    |> fold (ensure_fun thy arities eqngr) inst_params
+    |> fold (fn super_class => ensure_inst ctxt arities eqngr (super_class, tyco)) super_classes
+    |> fold (ensure_fun ctxt arities eqngr) inst_params
     |> fold_index (fn (k, classes) =>
-         add_classes thy arities eqngr (Inst (class, tyco), k) classes
+         add_classes ctxt arities eqngr (Inst (class, tyco), k) classes
          #> fold (fn super_class =>
-             add_dep thy arities eqngr (Inst (super_class, tyco), k)
+             add_dep ctxt arities eqngr (Inst (super_class, tyco), k)
              (Inst (class, tyco), k)) super_classes
          #> fold (fn inst_param =>
-             add_dep thy arities eqngr (Fun inst_param, k)
+             add_dep ctxt arities eqngr (Fun inst_param, k)
              (Inst (class, tyco), k)
              ) inst_params
          ) classess
   end
-and ensure_typmatch thy arities eqngr (Tyco tyco_styps) c_k vardeps_data =
+and ensure_typmatch ctxt arities eqngr (Tyco tyco_styps) c_k vardeps_data =
       vardeps_data
-      |> add_styp thy arities eqngr c_k tyco_styps
-  | ensure_typmatch thy arities eqngr (Var c_k') c_k vardeps_data =
+      |> add_styp ctxt arities eqngr c_k tyco_styps
+  | ensure_typmatch ctxt arities eqngr (Var c_k') c_k vardeps_data =
       vardeps_data
-      |> add_dep thy arities eqngr c_k c_k'
-  | ensure_typmatch thy arities eqngr Free c_k vardeps_data =
+      |> add_dep ctxt arities eqngr c_k c_k'
+  | ensure_typmatch ctxt arities eqngr Free c_k vardeps_data =
       vardeps_data
-and ensure_rhs thy arities eqngr (c', styps) vardeps_data =
+and ensure_rhs ctxt arities eqngr (c', styps) vardeps_data =
   vardeps_data
-  |> ensure_fun thy arities eqngr c'
+  |> ensure_fun ctxt arities eqngr c'
   |> fold_index (fn (k, styp) =>
-       ensure_typmatch thy arities eqngr styp (Fun c', k)) styps
-and ensure_fun thy arities eqngr c (vardeps_data as (_, (eqntab, _))) =
+       ensure_typmatch ctxt arities eqngr styp (Fun c', k)) styps
+and ensure_fun ctxt arities eqngr c (vardeps_data as (_, (eqntab, _))) =
   if Symtab.defined eqntab c then vardeps_data
   else let
-    val ((lhs, rhss), eqns) = obtain_eqns thy eqngr c;
+    val ((lhs, rhss), eqns) = obtain_eqns ctxt eqngr c;
     val rhss' = (map o apsnd o map) (styp_of (SOME (c, lhs))) rhss;
   in
     vardeps_data
     |> (apsnd o apfst) (Symtab.update_new (c, (lhs, eqns)))
     |> fold_index (fn (k, _) =>
          apfst (Vargraph.new_node ((Fun c, k), ([] ,[])))) lhs
-    |> fold_index (fn (k, (_, sort)) =>
-         add_classes thy arities eqngr (Fun c, k) (complete_proper_sort thy sort)) lhs
-    |> fold (ensure_rhs thy arities eqngr) rhss'
+    |> fold_index (fn (k, (_, sort)) => add_classes ctxt arities eqngr (Fun c, k)
+         (complete_proper_sort (Proof_Context.theory_of ctxt) sort)) lhs
+    |> fold (ensure_rhs ctxt arities eqngr) rhss'
   end;
 
 
@@ -413,11 +414,13 @@
 
 fun extend_arities_eqngr thy cs ts (arities, (eqngr : code_graph)) =
   let
+    val {pre, ...} = the_thmproc thy;
+    val ctxt = thy |> Proof_Context.init_global |> put_simpset pre;
     val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) =>
       insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts [];
     val (vardeps, (eqntab, insts)) = empty_vardeps_data
-      |> fold (ensure_fun thy arities eqngr) cs
-      |> fold (ensure_rhs thy arities eqngr) cs_rhss;
+      |> fold (ensure_fun ctxt arities eqngr) cs
+      |> fold (ensure_rhs ctxt arities eqngr) cs_rhss;
     val arities' = fold (add_arity thy vardeps) insts arities;
     val algebra = Sorts.subalgebra (Context.pretty_global thy) (is_proper_class thy)
       (AList.lookup (op =) arities') (Sign.classes_of thy);