# HG changeset patch
# User wenzelm
# Date 1433352305 -7200
# Node ID e201bd8973db8d748e513355ae84ecb9cbfab50e
# Parent  df3e916bcd26c294bf4d478f2d3490dc4e19a7f7
clarified context;

diff -r df3e916bcd26 -r e201bd8973db src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Tue Jun 02 23:00:50 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Wed Jun 03 19:25:05 2015 +0200
@@ -181,7 +181,7 @@
                   val (param_thm', ctxt'') = Thm.proof_attributes atts param_thm ctxt';
 
                   fun label_thm thm =
-                    Thm.cterm_of ctxt' (Free (nm, propT))
+                    Thm.cterm_of ctxt'' (Free (nm, propT))
                     |> Drule.mk_term
                     |> not (null abs_nms) ? Conjunction.intr thm
 
@@ -509,19 +509,18 @@
 (* Fix schematics in the goal *)
 fun focus_concl ctxt i goal =
   let
-    val ({context, concl, params, prems, asms, schematics}, goal') =
+    val ({context = ctxt', concl, params, prems, asms, schematics}, goal') =
       Subgoal.focus_params ctxt i goal;
 
-    val ((_, schematic_terms), context') =
-      Variable.import_inst true [Thm.term_of concl] context
-      |>> Thm.certify_inst (Thm.theory_of_thm goal');
+    val (inst, ctxt'') = Variable.import_inst true [Thm.term_of concl] ctxt';
+    val (_, schematic_terms) = Thm.certify_inst ctxt'' inst;
 
     val goal'' = Thm.instantiate ([], schematic_terms) goal';
     val concl' = Thm.instantiate_cterm ([], schematic_terms) concl;
     val (schematic_types, schematic_terms') = schematics;
     val schematics' = (schematic_types, schematic_terms @ schematic_terms');
   in
-    ({context = context', concl = concl', params = params, prems = prems,
+    ({context = ctxt'', concl = concl', params = params, prems = prems,
       schematics = schematics', asms = asms} : Subgoal.focus, goal'')
   end;
 
diff -r df3e916bcd26 -r e201bd8973db src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Tue Jun 02 23:00:50 2015 +0200
+++ b/src/HOL/Import/import_rule.ML	Wed Jun 03 19:25:05 2015 +0200
@@ -328,13 +328,14 @@
 
 fun store_thm binding thm thy =
   let
+    val ctxt = Proof_Context.init_global thy
     val thm = Drule.export_without_context_open thm
     val tvs = Term.add_tvars (Thm.prop_of thm) []
     val tns = map (fn (_, _) => "'") tvs
-    val nms = fst (fold_map Name.variant tns (Variable.names_of (Proof_Context.init_global thy)))
+    val nms = fst (fold_map Name.variant tns (Variable.names_of ctxt))
     val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs))
-    val cvs = map (Thm.global_ctyp_of thy) vs
-    val ctvs = map (Thm.global_ctyp_of thy) (map TVar tvs)
+    val cvs = map (Thm.ctyp_of ctxt) vs
+    val ctvs = map (Thm.ctyp_of ctxt) (map TVar tvs)
     val thm' = Thm.instantiate ((ctvs ~~ cvs), []) thm
   in
     snd (Global_Theory.add_thm ((binding, thm'), []) thy)
diff -r df3e916bcd26 -r e201bd8973db src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Jun 02 23:00:50 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Jun 03 19:25:05 2015 +0200
@@ -947,7 +947,7 @@
     val U = TFree ("'u", @{sort type})
     val y = Free (yname, U)
     val f' = absdummy (U --> T') (Bound 0 $ y)
-    val th' = Thm.certify_instantiate
+    val th' = Thm.certify_instantiate ctxt
       ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
        [((fst (dest_Var f), (U --> T') --> T'), f')]) th
     val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th']
@@ -1086,13 +1086,13 @@
               if not (fst (dest_Const pred) = fst (dest_Const pred')) then
                 raise Fail "Trying to instantiate another predicate"
               else ()
-          in Thm.certify_instantiate (subst_of (pred', pred), []) th end
+          in Thm.certify_instantiate ctxt' (subst_of (pred', pred), []) th end
         fun instantiate_ho_args th =
           let
             val (_, args') =
               (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) th
             val ho_args' = map dest_Var (ho_args_of_typ T args')
-          in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
+          in Thm.certify_instantiate ctxt' ([], ho_args' ~~ ho_args) th end
         val outp_pred =
           Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
         val ((_, ths'), ctxt1) =
diff -r df3e916bcd26 -r e201bd8973db src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Tue Jun 02 23:00:50 2015 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML	Wed Jun 03 19:25:05 2015 +0200
@@ -697,7 +697,7 @@
     val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
                 |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
     val thm2 = thm1
-      |> Thm.certify_instantiate (instT, [])
+      |> Thm.certify_instantiate ctxt (instT, [])
       |> Raw_Simplifier.rewrite_rule ctxt pre_simps
     val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
     val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
@@ -733,7 +733,7 @@
     val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
                 |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
     val thm2 = thm1
-      |> Thm.certify_instantiate (instT, [])
+      |> Thm.certify_instantiate ctxt (instT, [])
       |> Raw_Simplifier.rewrite_rule ctxt pre_simps
     val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
     val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
diff -r df3e916bcd26 -r e201bd8973db src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Jun 02 23:00:50 2015 +0200
+++ b/src/Pure/Isar/code.ML	Wed Jun 03 19:25:05 2015 +0200
@@ -635,19 +635,19 @@
     else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names)
   end;
 
-fun desymbolize_tvars thms =
+fun desymbolize_tvars thy thms =
   let
     val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
     val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs;
-  in map (Thm.certify_instantiate (tvar_subst, [])) thms end;
+  in map (Thm.global_certify_instantiate thy (tvar_subst, [])) thms end;
 
-fun desymbolize_vars thm =
+fun desymbolize_vars thy thm =
   let
     val vs = Term.add_vars (Thm.prop_of thm) [];
     val var_subst = mk_desymbolization I I Var vs;
-  in Thm.certify_instantiate ([], var_subst) thm end;
+  in Thm.global_certify_instantiate thy ([], var_subst) thm end;
 
-fun canonize_thms thy = desymbolize_tvars #> same_arity thy #> map desymbolize_vars;
+fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy);
 
 
 (* abstype certificates *)
@@ -706,7 +706,7 @@
   in
     thm
     |> Thm.varifyT_global
-    |> Thm.certify_instantiate (inst, [])
+    |> Thm.global_certify_instantiate thy (inst, [])
     |> pair subst
   end;
 
@@ -771,7 +771,7 @@
         val sorts = map_transpose inter_sorts vss;
         val vts = Name.invent_names Name.context Name.aT sorts;
         val thms' =
-          map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms;
+          map2 (fn vs => Thm.certify_instantiate ctxt (vs ~~ map TFree vts, [])) vss thms;
         val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms'))));
         fun head_conv ct = if can Thm.dest_comb ct
           then Conv.fun_conv head_conv ct
diff -r df3e916bcd26 -r e201bd8973db src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jun 02 23:00:50 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Jun 03 19:25:05 2015 +0200
@@ -935,7 +935,7 @@
 
 fun comp_hhf_tac ctxt th i st =
   PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
-    (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
+    (false, Drule.lift_all ctxt (Thm.cprem_of st i) th, 0) i) st;
 
 fun comp_incr_tac _ [] _ = no_tac
   | comp_incr_tac ctxt (th :: ths) i =
diff -r df3e916bcd26 -r e201bd8973db src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Jun 02 23:00:50 2015 +0200
+++ b/src/Pure/drule.ML	Wed Jun 03 19:25:05 2015 +0200
@@ -17,7 +17,7 @@
   val forall_intr_vars: thm -> thm
   val forall_elim_list: cterm list -> thm -> thm
   val gen_all: int -> thm -> thm
-  val lift_all: cterm -> thm -> thm
+  val lift_all: Proof.context -> cterm -> thm -> thm
   val implies_elim_list: thm -> thm list -> thm
   val implies_intr_list: cterm list -> thm -> thm
   val instantiate_normalize: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
@@ -192,9 +192,12 @@
 
 (*lift vars wrt. outermost goal parameters
   -- reverses the effect of gen_all modulo higher-order unification*)
-fun lift_all goal th =
+fun lift_all ctxt raw_goal raw_th =
   let
-    val thy = Theory.merge (Thm.theory_of_cterm goal, Thm.theory_of_thm th);
+    val thy = Proof_Context.theory_of ctxt;
+    val goal = Thm.transfer_cterm thy raw_goal;
+    val th = Thm.transfer thy raw_th;
+
     val maxidx = Thm.maxidx_of th;
     val ps = outer_params (Thm.term_of goal)
       |> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T));
@@ -204,8 +207,8 @@
       |> map (fn (xi, T) => ((xi, T), Term.list_comb (Var (xi, Ts ---> T), ps)));
   in
     th
-    |> Thm.instantiate (Thm.certify_inst thy ([], inst))
-    |> fold_rev (Thm.forall_intr o Thm.global_cterm_of thy) ps
+    |> Thm.certify_instantiate ctxt ([], inst)
+    |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) ps
   end;
 
 (*direct generalization*)
@@ -225,10 +228,8 @@
   | zero_var_indexes_list ths =
       let
         val thy = Theory.merge_list (map Thm.theory_of_thm ths);
-        val inst =
-          Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths)
-          |> Thm.certify_inst thy;
-      in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate inst) ths end;
+        val insts = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
+      in map (Thm.adjust_maxidx_thm ~1 o Thm.global_certify_instantiate thy insts) ths end;
 
 val zero_var_indexes = singleton zero_var_indexes_list;
 
@@ -359,7 +360,7 @@
   Context.>>> (Context.map_theory_result (Global_Theory.store_thm_open (name, th)));
 
 fun store_standard_thm name th = store_thm name (export_without_context th);
-fun store_standard_thm_open name thm = store_thm_open name (export_without_context_open thm);
+fun store_standard_thm_open name th = store_thm_open name (export_without_context_open th);
 
 val reflexive_thm =
   let val cx = certify (Var(("x",0),TVar(("'a",0),[])))
diff -r df3e916bcd26 -r e201bd8973db src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Jun 02 23:00:50 2015 +0200
+++ b/src/Pure/more_thm.ML	Wed Jun 03 19:25:05 2015 +0200
@@ -60,10 +60,15 @@
   val elim_implies: thm -> thm -> thm
   val forall_elim_var: int -> thm -> thm
   val forall_elim_vars: int -> thm -> thm
-  val certify_inst: theory ->
+  val global_certify_inst: theory ->
     ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
     (ctyp * ctyp) list * (cterm * cterm) list
-  val certify_instantiate:
+  val global_certify_instantiate: theory ->
+    ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
+  val certify_inst: Proof.context ->
+    ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
+    (ctyp * ctyp) list * (cterm * cterm) list
+  val certify_instantiate: Proof.context ->
     ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
   val forall_intr_frees: thm -> thm
   val unvarify_global: thm -> thm
@@ -351,12 +356,19 @@
 
 (* certify_instantiate *)
 
-fun certify_inst thy (instT, inst) =
+fun global_certify_inst thy (instT, inst) =
  (map (fn (v, T) => apply2 (Thm.global_ctyp_of thy) (TVar v, T)) instT,
   map (fn (v, t) => apply2 (Thm.global_cterm_of thy) (Var v, t)) inst);
 
-fun certify_instantiate insts th =
-  Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th;
+fun global_certify_instantiate thy insts th =
+  Thm.instantiate (global_certify_inst thy insts) th;
+
+fun certify_inst ctxt (instT, inst) =
+ (map (fn (v, T) => apply2 (Thm.ctyp_of ctxt) (TVar v, T)) instT,
+  map (fn (v, t) => apply2 (Thm.cterm_of ctxt) (Var v, t)) inst);
+
+fun certify_instantiate ctxt insts th =
+  Thm.instantiate (certify_inst ctxt insts) th;
 
 
 (* forall_intr_frees: generalization over all suitable Free variables *)
@@ -375,6 +387,8 @@
 
 fun unvarify_global th =
   let
+    val thy = Thm.theory_of_thm th;
+
     val prop = Thm.full_prop_of th;
     val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th)
       handle TERM (msg, _) => raise THM (msg, 0, [th]);
@@ -383,7 +397,7 @@
     val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
       let val T' = Term_Subst.instantiateT instT T
       in (((a, i), T'), Free ((a, T'))) end);
-  in certify_instantiate (instT, inst) th end;
+  in global_certify_instantiate thy (instT, inst) th end;
 
 
 (* close_derivation *)
@@ -444,7 +458,7 @@
     val _ = Sign.no_vars ctxt prop;
     val (strip, recover, prop') = stripped_sorts thy prop;
     val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
-    val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.global_ctyp_of thy T, S)) strip;
+    val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of ctxt T, S)) strip;
 
     val thy' = thy
       |> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop'));
@@ -461,7 +475,7 @@
 fun add_def ctxt unchecked overloaded (b, prop) thy =
   let
     val _ = Sign.no_vars ctxt prop;
-    val prems = map (Thm.global_cterm_of thy) (Logic.strip_imp_prems prop);
+    val prems = map (Thm.cterm_of ctxt) (Logic.strip_imp_prems prop);
     val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
 
     val thy' = Theory.add_def ctxt unchecked overloaded (b, concl') thy;
diff -r df3e916bcd26 -r e201bd8973db src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Tue Jun 02 23:00:50 2015 +0200
+++ b/src/Pure/subgoal.ML	Wed Jun 03 19:25:05 2015 +0200
@@ -31,7 +31,9 @@
 
 fun gen_focus (do_prems, do_concl) ctxt i raw_st =
   let
-    val st = Simplifier.norm_hhf_protect ctxt raw_st;
+    val st = raw_st
+      |> Thm.transfer (Proof_Context.theory_of ctxt)
+      |> Simplifier.norm_hhf_protect ctxt;
     val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
     val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
 
@@ -40,9 +42,8 @@
       else ([], goal);
     val text = asms @ (if do_concl then [concl] else []);
 
-    val ((_, schematic_terms), ctxt3) =
-      Variable.import_inst true (map Thm.term_of text) ctxt2
-      |>> Thm.certify_inst (Thm.theory_of_thm raw_st);
+    val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
+    val (_, schematic_terms) = Thm.certify_inst ctxt3 inst;
 
     val schematics = (schematic_types, schematic_terms);
     val asms' = map (Thm.instantiate_cterm schematics) asms;
diff -r df3e916bcd26 -r e201bd8973db src/Pure/variable.ML
--- a/src/Pure/variable.ML	Tue Jun 02 23:00:50 2015 +0200
+++ b/src/Pure/variable.ML	Wed Jun 03 19:25:05 2015 +0200
@@ -578,9 +578,8 @@
 
 fun importT ths ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
-    val insts' as (instT', _) = Thm.certify_inst thy (instT, []);
+    val insts' as (instT', _) = Thm.certify_inst ctxt' (instT, []);
     val ths' = map (Thm.instantiate insts') ths;
   in ((instT', ths'), ctxt') end;
 
@@ -592,9 +591,8 @@
 
 fun import is_open ths ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val (insts, ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
-    val insts' = Thm.certify_inst thy insts;
+    val insts' = Thm.certify_inst ctxt' insts;
     val ths' = map (Thm.instantiate insts') ths;
   in ((insts', ths'), ctxt') end;
 
diff -r df3e916bcd26 -r e201bd8973db src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Tue Jun 02 23:00:50 2015 +0200
+++ b/src/Tools/Code/code_preproc.ML	Wed Jun 03 19:25:05 2015 +0200
@@ -178,7 +178,7 @@
     if eq_list (eq_fst (op =)) (vs_normalized, vs_original)
     then (I, ct)
     else
-     (Thm.certify_instantiate (normalization, []) o Thm.varifyT_global,
+     (Thm.certify_instantiate ctxt (normalization, []) o Thm.varifyT_global,
       Thm.cterm_of ctxt (map_types normalize t))
   end;