# HG changeset patch
# User wenzelm
# Date 1438118953 -7200
# Node ID 31e08fe243f14e20b57479c744fcfc41d3ec2cdd
# Parent  53d8c91c86ec304f965849ebc83ca34c6d9de97f# Parent  695cf1fab6cc5ac1aedfc3781523df4556b53bdf
merged

diff -r 53d8c91c86ec -r 31e08fe243f1 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/FOL/simpdata.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -50,8 +50,7 @@
        | _ => [th])
   in atoms end;
 
-fun mksimps pairs ctxt =
-  map mk_eq o mk_atomize pairs o Drule.gen_all (Variable.maxidx_of ctxt);
+fun mksimps pairs ctxt = map mk_eq o mk_atomize pairs o Variable.gen_all ctxt;
 
 
 (** make simplification procedures for quantifier elimination **)
diff -r 53d8c91c86ec -r 31e08fe243f1 src/HOL/Decision_Procs/ferrante_rackoff.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -206,7 +206,7 @@
    val pcv = Simplifier.rewrite (put_simpset ss' ctxt);
    val postcv = Simplifier.rewrite (put_simpset ss ctxt);
    val nnf = K (nnf_conv ctxt then_conv postcv)
-   val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Thm.add_cterm_frees tm [])
+   val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Drule.cterm_add_frees tm [])
                   (isolate_conv ctxt) nnf
                   (fn vs => ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt,
                                                whatis = whatis, simpset = ss}) vs
diff -r 53d8c91c86ec -r 31e08fe243f1 src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -191,7 +191,7 @@
   in
     fn p =>
       Qelim.gen_qelim_conv pcv pcv dnfex_conv cons
-        (Thm.add_cterm_frees p []) (K Thm.reflexive) (K Thm.reflexive)
+        (Drule.cterm_add_frees p []) (K Thm.reflexive) (K Thm.reflexive)
         (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
   end;
 
diff -r 53d8c91c86ec -r 31e08fe243f1 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -900,9 +900,9 @@
         then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm)
         else raise Failure "substitutable_monomial"
     | @{term "op + :: real => _"}$_$_ =>
-         (substitutable_monomial (Thm.add_cterm_frees (Thm.dest_arg tm) fvs) (Thm.dest_arg1 tm)
+         (substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg tm) fvs) (Thm.dest_arg1 tm)
            handle Failure _ =>
-            substitutable_monomial (Thm.add_cterm_frees (Thm.dest_arg1 tm) fvs) (Thm.dest_arg tm))
+            substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg1 tm) fvs) (Thm.dest_arg tm))
     | _ => raise Failure "substitutable_monomial")
 
   fun isolate_variable v th =
diff -r 53d8c91c86ec -r 31e08fe243f1 src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -2625,7 +2625,8 @@
 
 fun simplify_defn ctxt strict congs wfs pats def0 =
   let
-    val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
+    val thy = Proof_Context.theory_of ctxt;
+    val def = Thm.unvarify_global thy def0 RS meta_eq_to_obj_eq
     val {rules, rows, TCs, full_pats_TCs} = Prim.post_definition ctxt congs (def, pats)
     val {lhs=f,rhs} = USyntax.dest_eq (concl def)
     val (_,[R,_]) = USyntax.strip_comb rhs
diff -r 53d8c91c86ec -r 31e08fe243f1 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -800,7 +800,7 @@
 
               fun make_sel_thm xs' case_thm sel_def =
                 zero_var_indexes
-                  (Drule.gen_all (Variable.maxidx_of lthy)
+                  (Variable.gen_all lthy
                     (Drule.rename_bvars'
                       (map (SOME o fst) xs')
                       (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
diff -r 53d8c91c86ec -r 31e08fe243f1 src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -27,7 +27,7 @@
   let
     val thms as thm1 :: _ = raw_thms
       |> Conjunction.intr_balanced
-      |> Thm.unvarify_global
+      |> Thm.unvarify_global thy
       |> Conjunction.elim_balanced (length raw_thms)
       |> map Simpdata.mk_meta_eq
       |> map Drule.zero_var_indexes;
@@ -53,7 +53,7 @@
     fun true_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term True});
     fun false_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term False});
 
-    val monomorphic_prop_of = Thm.prop_of o Thm.unvarify_global o Drule.zero_var_indexes;
+    val monomorphic_prop_of = Thm.prop_of o Thm.unvarify_global thy o Drule.zero_var_indexes;
 
     fun massage_inject (tp $ (eqv $ (_ $ t $ u) $ rhs)) = tp $ (eqv $ mk_fcT_eq (t, u) $ rhs);
     fun massage_distinct (tp $ (_ $ (_ $ t $ u))) = [tp $ false_eq (t, u), tp $ false_eq (u, t)];
diff -r 53d8c91c86ec -r 31e08fe243f1 src/HOL/Tools/Qelim/qelim.ML
--- a/src/HOL/Tools/Qelim/qelim.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -65,7 +65,7 @@
 
 fun standard_qelim_conv ctxt atcv ncv qcv p =
   let val pcv = pcv ctxt
-  in gen_qelim_conv pcv pcv pcv cons (Thm.add_cterm_frees p []) atcv ncv qcv p end
+  in gen_qelim_conv pcv pcv pcv cons (Drule.cterm_add_frees p []) atcv ncv qcv p end
 
 end;
 
diff -r 53d8c91c86ec -r 31e08fe243f1 src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -35,12 +35,13 @@
 
 fun find_unused_assms ctxt thy_name =
   let
+    val thy = Proof_Context.theory_of ctxt
     val ctxt' = ctxt
        |> Config.put Quickcheck.abort_potential true
        |> Config.put Quickcheck.quiet true
     val all_thms =
       filter (fn (s, _) => length (Long_Name.explode s) = 2)  (* FIXME !? *)
-        (thms_of (Proof_Context.theory_of ctxt) thy_name)
+        (thms_of thy thy_name)
     fun check_single conjecture =
       (case try (Quickcheck.test_terms ctxt' (true, true) []) [(conjecture, [])] of
         SOME (SOME _) => false
@@ -53,7 +54,7 @@
             if member (op =) S x then I
             else insert (eq_set (op =)) (insert (op =) x S)) X) Ss []
     fun check (s, th) =
-      (case Logic.strip_horn (Thm.prop_of (Thm.unvarify_global th)) of
+      (case Logic.strip_horn (Thm.prop_of (Thm.unvarify_global thy th)) of
         ([], _) => (s, NONE)
       | (ts, t) =>
           let
diff -r 53d8c91c86ec -r 31e08fe243f1 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -178,7 +178,7 @@
           else ()
       in
         arg
-        |> apsnd Thm.unvarify_global
+        |> apsnd (Thm.unvarify_global thy)
         |> process_all (zip3 alt_names rew_imps frees)
       end
 
diff -r 53d8c91c86ec -r 31e08fe243f1 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -147,7 +147,7 @@
             | _ => AbsP ("H", SOME p, prf)))
           (rec_fns ~~ Thm.prems_of thm)
           (Proofterm.proof_combP
-            (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
+            (Reconstruct.proof_of thy' thm', map PBound (length prems - 1 downto 0))));
 
     val r' =
       if null is then r
@@ -212,10 +212,10 @@
               (AbsP ("H", SOME (Logic.varify_global p), prf)))
           (prems ~~ rs)
           (Proofterm.proof_combP
-            (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
+            (Reconstruct.proof_of thy' thm', map PBound (length prems - 1 downto 0))));
     val prf' =
       Extraction.abs_corr_shyps thy' exhaust []
-        (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
+        (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Reconstruct.proof_of thy' exhaust);
     val r' =
       Logic.varify_global (Abs ("y", T,
         (fold_rev (Term.abs o dest_Free) rs
diff -r 53d8c91c86ec -r 31e08fe243f1 src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Tools/groebner.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -532,7 +532,7 @@
  fun simp_ex_conv ctxt =
    Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)})
 
-fun frees t = Thm.add_cterm_frees t [];
+fun frees t = Drule.cterm_add_frees t [];
 fun free_in v t = member op aconvc (frees t) v;
 
 val vsubst = let
@@ -741,7 +741,7 @@
     Thm.apply
       (Drule.cterm_rule (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] [])
         @{cpat "All:: (?'a => bool) => _"}) (Thm.lambda x p)
-  val avs = Thm.add_cterm_frees tm []
+  val avs = Drule.cterm_add_frees tm []
   val P' = fold mk_forall avs tm
   val th1 = initial_conv ctxt (mk_neg P')
   val (evs,bod) = strip_exists(concl th1) in
@@ -797,7 +797,7 @@
    val mons = striplist(dest_binary ring_add_tm) t
   in member (op aconvc) mons v andalso
     forall (fn m => v aconvc m
-          orelse not(member (op aconvc) (Thm.add_cterm_frees m []) v)) mons
+          orelse not(member (op aconvc) (Drule.cterm_add_frees m []) v)) mons
   end
 
   fun isolate_variable vars tm =
diff -r 53d8c91c86ec -r 31e08fe243f1 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -20,7 +20,7 @@
   | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
 
 fun prf_of thy thm =
-  Reconstruct.proof_of thm
+  Reconstruct.proof_of thy thm
   |> Reconstruct.expand_proof thy [("", NONE)];  (* FIXME *)
 
 fun subsets [] = [[]]
diff -r 53d8c91c86ec -r 31e08fe243f1 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Tools/simpdata.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -112,8 +112,7 @@
       end;
   in atoms end;
 
-fun mksimps pairs ctxt =
-  map_filter (try mk_eq) o mk_atomize ctxt pairs o Drule.gen_all (Variable.maxidx_of ctxt);
+fun mksimps pairs ctxt = map_filter (try mk_eq) o mk_atomize ctxt pairs o Variable.gen_all ctxt;
 
 fun unsafe_solver_tac ctxt =
   let
diff -r 53d8c91c86ec -r 31e08fe243f1 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Provers/classical.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -147,6 +147,7 @@
 fun classical_rule ctxt rule =
   if is_some (Object_Logic.elim_concl ctxt rule) then
     let
+      val thy = Proof_Context.theory_of ctxt;
       val rule' = rule RS Data.classical;
       val concl' = Thm.concl_of rule';
       fun redundant_hyp goal =
@@ -161,7 +162,7 @@
           else all_tac))
         |> Seq.hd
         |> Drule.zero_var_indexes;
-    in if Thm.equiv_thm (rule, rule'') then rule else rule'' end
+    in if Thm.equiv_thm thy (rule, rule'') then rule else rule'' end
   else rule;
 
 (*flatten nested meta connectives in prems*)
diff -r 53d8c91c86ec -r 31e08fe243f1 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/Isar/class.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -748,7 +748,7 @@
 
 fun intro_classes_tac ctxt facts st =
   let
-    val thy = Thm.theory_of_thm st;
+    val thy = Proof_Context.theory_of ctxt;
     val classes = Sign.all_classes thy;
     val class_trivs = map (Thm.class_triv thy) classes;
     val class_intros = map_filter (try (#intro o Axclass.get_info thy)) classes;
diff -r 53d8c91c86ec -r 31e08fe243f1 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/Isar/local_defs.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -129,30 +129,23 @@
   --------------
        B as
 *)
-fun export inner outer =    (*beware of closure sizes*)
+fun export inner outer th =
   let
-    val exp = Assumption.export false inner outer;
-    val exp_term = Assumption.export_term inner outer;
-    val asms = Assumption.local_assms_of inner outer;
-  in
-    fn th =>
-      let
-        val th' = exp th;
-        val defs_asms = asms
-          |> filter_out (Drule.is_sort_constraint o Thm.term_of)
-          |> map (Thm.assume #> (fn asm =>
-            (case try (head_of_def o Thm.prop_of) asm of
-              NONE => (asm, false)
-            | SOME x =>
-                let val t = Free x in
-                  (case try exp_term t of
-                    NONE => (asm, false)
-                  | SOME u =>
-                      if t aconv u then (asm, false)
-                      else (Drule.abs_def (Drule.gen_all (Variable.maxidx_of outer) asm), true))
-                end)));
-      in (apply2 (map #1) (List.partition #2 defs_asms), th') end
-  end;
+    val defs_asms =
+      Assumption.local_assms_of inner outer
+      |> filter_out (Drule.is_sort_constraint o Thm.term_of)
+      |> map (Thm.assume #> (fn asm =>
+        (case try (head_of_def o Thm.prop_of) asm of
+          NONE => (asm, false)
+        | SOME x =>
+            let val t = Free x in
+              (case try (Assumption.export_term inner outer) t of
+                NONE => (asm, false)
+              | SOME u =>
+                  if t aconv u then (asm, false)
+                  else (Drule.abs_def (Variable.gen_all outer asm), true))
+            end)));
+  in (apply2 (map #1) (List.partition #2 defs_asms), Assumption.export false inner outer th) end;
 
 (*
   [xs, xs == as]
diff -r 53d8c91c86ec -r 31e08fe243f1 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/Isar/object_logic.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -203,7 +203,7 @@
 
 fun gen_rulify full ctxt =
   Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify ctxt))
-  #> Drule.gen_all (Variable.maxidx_of ctxt)
+  #> Variable.gen_all ctxt
   #> Thm.strip_shyps
   #> Drule.zero_var_indexes;
 
diff -r 53d8c91c86ec -r 31e08fe243f1 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -501,7 +501,7 @@
       (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
         handle THM _ => err_lost ())
       |> Drule.flexflex_unique (SOME ctxt)
-      |> Thm.check_shyps (Variable.sorts_of ctxt)
+      |> Thm.check_shyps ctxt (Variable.sorts_of ctxt)
       |> Thm.check_hyps (Context.Proof ctxt);
 
     val goal_propss = filter_out null propss;
diff -r 53d8c91c86ec -r 31e08fe243f1 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -769,9 +769,9 @@
 
       | extr d vs ts Ts hs _ defs = error "extr: bad proof";
 
-    fun prep_thm vs thm =
+    fun prep_thm vs raw_thm =
       let
-        val thy = Thm.theory_of_thm thm;
+        val thm = Thm.transfer thy raw_thm;
         val prop = Thm.prop_of thm;
         val prf = Thm.proof_of thm;
         val name = Thm.derivation_name thm;
diff -r 53d8c91c86ec -r 31e08fe243f1 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -14,7 +14,7 @@
   val read_term: theory -> bool -> typ -> string -> term
   val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
   val proof_syntax: Proofterm.proof -> theory -> theory
-  val proof_of: bool -> thm -> Proofterm.proof
+  val proof_of: theory -> bool -> thm -> Proofterm.proof
   val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
   val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T
 end;
@@ -235,9 +235,9 @@
       (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names)
   end;
 
-fun proof_of full thm =
+fun proof_of thy full raw_thm =
   let
-    val thy = Thm.theory_of_thm thm;
+    val thm = Thm.transfer thy raw_thm;
     val prop = Thm.full_prop_of thm;
     val prf = Thm.proof_of thm;
     val prf' =
@@ -253,6 +253,6 @@
     (term_of_proof prf);
 
 fun pretty_proof_of ctxt full th =
-  pretty_proof ctxt (proof_of full th);
+  pretty_proof ctxt (proof_of (Proof_Context.theory_of ctxt) full th);
 
 end;
diff -r 53d8c91c86ec -r 31e08fe243f1 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -10,7 +10,7 @@
   val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
   val prop_of' : term list -> Proofterm.proof -> term
   val prop_of : Proofterm.proof -> term
-  val proof_of : thm -> Proofterm.proof
+  val proof_of : theory -> thm -> Proofterm.proof
   val expand_proof : theory -> (string * term option) list ->
     Proofterm.proof -> Proofterm.proof
 end;
@@ -324,8 +324,9 @@
 val prop_of' = Envir.beta_eta_contract oo prop_of0;
 val prop_of = prop_of' [];
 
-fun proof_of thm =
-  reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
+fun proof_of thy raw_thm =
+  let val thm = Thm.transfer thy raw_thm
+  in reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm) end;
 
 
 
diff -r 53d8c91c86ec -r 31e08fe243f1 src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/conjunction.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -76,8 +76,7 @@
 val A_B = read_prop "A &&& B";
 
 val conjunction_def =
-  Thm.unvarify_global
-    (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
+  Thm.unvarify_axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def";
 
 fun conjunctionD which =
   Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
@@ -138,8 +137,13 @@
 
 local
 
-fun conjs thy n =
-  let val As = map (fn A => Thm.global_cterm_of thy (Free (A, propT))) (Name.invent Name.context "A" n)
+val bootstrap_thy = Context.theory_of (Context.the_thread_data ());
+
+fun conjs n =
+  let
+    val As =
+      map (fn A => Thm.global_cterm_of bootstrap_thy (Free (A, propT)))
+        (Name.invent Name.context "A" n);
   in (As, mk_conjunction_balanced As) end;
 
 val B = read_prop "B";
@@ -159,8 +163,7 @@
   if n < 2 then th
   else
     let
-      val thy = Thm.theory_of_thm th;
-      val (As, C) = conjs thy n;
+      val (As, C) = conjs n;
       val D = Drule.mk_implies (C, B);
     in
       comp_rule th
@@ -177,8 +180,7 @@
   if n < 2 then th
   else
     let
-      val thy = Thm.theory_of_thm th;
-      val (As, C) = conjs thy n;
+      val (As, C) = conjs n;
       val D = Drule.list_implies (As, B);
     in
       comp_rule th
diff -r 53d8c91c86ec -r 31e08fe243f1 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/drule.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -16,7 +16,6 @@
   val forall_intr_list: cterm list -> thm -> thm
   val forall_intr_vars: thm -> thm
   val forall_elim_list: cterm list -> thm -> thm
-  val gen_all: int -> 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
@@ -53,6 +52,7 @@
 signature DRULE =
 sig
   include BASIC_DRULE
+  val outer_params: term -> (string * typ) list
   val generalize: string list * string list -> thm -> thm
   val list_comb: cterm * cterm list -> cterm
   val strip_comb: cterm -> cterm * cterm list
@@ -91,6 +91,8 @@
   val mk_term: cterm -> thm
   val dest_term: thm -> cterm
   val cterm_rule: (thm -> thm) -> cterm -> cterm
+  val cterm_add_frees: cterm -> cterm list -> cterm list
+  val cterm_add_vars: cterm -> cterm list -> cterm list
   val dummy_thm: thm
   val is_sort_constraint: term -> bool
   val sort_constraintI: thm
@@ -174,24 +176,12 @@
 val forall_intr_list = fold_rev Thm.forall_intr;
 
 (*Generalization over Vars -- canonical order*)
-fun forall_intr_vars th =
-  fold Thm.forall_intr
-    (map (Thm.global_cterm_of (Thm.theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th [])) th;
+fun forall_intr_vars th = fold Thm.forall_intr (Thm.add_vars th []) th;
 
 fun outer_params t =
   let val vs = Term.strip_all_vars t
   in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end;
 
-(*generalize outermost parameters*)
-fun gen_all maxidx0 th =
-  let
-    val thy = Thm.theory_of_thm th;
-    val maxidx = Thm.maxidx_thm th maxidx0;
-    val prop = Thm.prop_of th;
-    fun elim (x, T) =
-      Thm.forall_elim (Thm.global_cterm_of thy (Var ((x, maxidx + 1), T)));
-  in fold elim (outer_params prop) th end;
-
 (*lift vars wrt. outermost goal parameters
   -- reverses the effect of gen_all modulo higher-order unification*)
 fun lift_all ctxt raw_goal raw_th =
@@ -576,7 +566,7 @@
 
 local
   val A = certify (Free ("A", propT));
-  val axiom = Thm.unvarify_global o Thm.axiom (Context.the_theory (Context.the_thread_data ()));
+  val axiom = Thm.unvarify_axiom (Context.the_theory (Context.the_thread_data ()));
   val prop_def = axiom "Pure.prop_def";
   val term_def = axiom "Pure.term_def";
   val sort_constraint_def = axiom "Pure.sort_constraint_def";
@@ -631,6 +621,9 @@
 
 fun cterm_rule f = dest_term o f o mk_term;
 
+val cterm_add_frees = Thm.add_frees o mk_term;
+val cterm_add_vars = Thm.add_vars o mk_term;
+
 val dummy_thm = mk_term (certify Term.dummy_prop);
 
 
@@ -647,7 +640,7 @@
   store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", @{here})))
     (Thm.equal_intr
       (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA)
-        (Thm.unvarify_global sort_constraintI)))
+        (Thm.unvarify_global (Context.the_theory (Context.the_thread_data ())) sort_constraintI)))
       (implies_intr_list [A, C] (Thm.assume A)));
 
 end;
diff -r 53d8c91c86ec -r 31e08fe243f1 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/goal.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -214,7 +214,7 @@
             val res =
               (finish ctxt' st
                 |> Drule.flexflex_unique (SOME ctxt')
-                |> Thm.check_shyps sorts
+                |> Thm.check_shyps ctxt' sorts
                 |> Thm.check_hyps (Context.Proof ctxt'))
               handle THM (msg, _, _) => err msg | ERROR msg => err msg;
           in
diff -r 53d8c91c86ec -r 31e08fe243f1 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/more_thm.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -21,7 +21,8 @@
   structure Ctermtab: TABLE
   structure Thmtab: TABLE
   val aconvc: cterm * cterm -> bool
-  val add_cterm_frees: cterm -> cterm list -> cterm list
+  val add_frees: thm -> cterm list -> cterm list
+  val add_vars: thm -> cterm list -> cterm list
   val all_name: string * cterm -> cterm -> cterm
   val all: cterm -> cterm -> cterm
   val mk_binop: cterm -> cterm -> cterm -> cterm
@@ -39,10 +40,10 @@
   val eq_thm: thm * thm -> bool
   val eq_thm_prop: thm * thm -> bool
   val eq_thm_strict: thm * thm -> bool
-  val equiv_thm: thm * thm -> bool
+  val equiv_thm: theory -> thm * thm -> bool
   val class_triv: theory -> class -> thm
   val of_sort: ctyp * sort -> thm list
-  val check_shyps: sort list -> thm -> thm
+  val check_shyps: Proof.context -> sort list -> thm -> thm
   val is_dummy: thm -> bool
   val plain_prop_of: thm -> term
   val add_thm: thm -> thm list -> thm list
@@ -62,7 +63,8 @@
   val forall_elim_vars: int -> thm -> thm
   val instantiate': ctyp option list -> cterm option list -> thm -> thm
   val forall_intr_frees: thm -> thm
-  val unvarify_global: thm -> thm
+  val unvarify_global: theory -> thm -> thm
+  val unvarify_axiom: theory -> string -> thm
   val close_derivation: thm -> thm
   val rename_params_rule: string list * int -> thm -> thm
   val rename_boundvars: term -> term -> thm -> thm
@@ -112,13 +114,8 @@
 
 val op aconvc = op aconv o apply2 Thm.term_of;
 
-fun add_cterm_frees ct =
-  let
-    val thy = Thm.theory_of_cterm ct;
-    val t = Thm.term_of ct;
-  in
-    Term.fold_aterms (fn v as Free _ => insert (op aconvc) (Thm.global_cterm_of thy v) | _ => I) t
-  end;
+val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a);
+val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a);
 
 
 (* cterm constructors and destructors *)
@@ -209,8 +206,8 @@
 
 (* pattern equivalence *)
 
-fun equiv_thm ths =
-  Pattern.equiv (Theory.merge (apply2 Thm.theory_of_thm ths)) (apply2 Thm.full_prop_of ths);
+fun equiv_thm thy ths =
+  Pattern.equiv thy (apply2 (Thm.full_prop_of o Thm.transfer thy) ths);
 
 
 (* type classes and sorts *)
@@ -220,15 +217,14 @@
 
 fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S;
 
-fun check_shyps sorts raw_th =
+fun check_shyps ctxt sorts raw_th =
   let
     val th = Thm.strip_shyps raw_th;
-    val prt_sort = Syntax.pretty_sort_global (Thm.theory_of_thm th);
     val pending = Sorts.subtract sorts (Thm.extra_shyps th);
   in
     if null pending then th
     else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" ::
-      Pretty.brk 1 :: Pretty.commas (map prt_sort pending))))
+      Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) pending))))
   end;
 
 
@@ -369,20 +365,20 @@
 
 fun forall_intr_frees th =
   let
-    val thy = Thm.theory_of_thm th;
     val {prop, hyps, tpairs, ...} = Thm.rep_thm th;
     val fixed = fold Term.add_frees (Thm.terms_of_tpairs tpairs @ hyps) [];
-    val frees = Term.fold_aterms (fn Free v =>
-      if member (op =) fixed v then I else insert (op =) v | _ => I) prop [];
-  in fold (Thm.forall_intr o Thm.global_cterm_of thy o Free) frees th end;
+    val frees =
+      Thm.fold_atomic_cterms (fn a =>
+        (case Thm.term_of a of
+          Free v => not (member (op =) fixed v) ? insert (op aconvc) a
+        | _ => I)) th [];
+  in fold Thm.forall_intr frees th end;
 
 
 (* unvarify_global: global schematic variables *)
 
-fun unvarify_global th =
+fun unvarify_global thy 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]);
@@ -393,6 +389,8 @@
       in (((a, i), T'), Thm.global_cterm_of thy (Free ((a, T')))) end);
   in Thm.instantiate (map (apsnd (Thm.global_ctyp_of thy)) instT, inst) th end;
 
+fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy;
+
 
 (* close_derivation *)
 
@@ -462,7 +460,7 @@
     val axm' = Thm.axiom thy' axm_name;
     val thm =
       Thm.instantiate (recover, []) axm'
-      |> unvarify_global
+      |> unvarify_global thy'
       |> fold elim_implies of_sorts;
   in ((axm_name, thm), thy') end;
 
@@ -479,7 +477,7 @@
     val axm' = Thm.axiom thy' axm_name;
     val thm =
       Thm.instantiate (recover, []) axm'
-      |> unvarify_global
+      |> unvarify_global thy'
       |> fold_rev Thm.implies_intr prems;
   in ((axm_name, thm), thy') end;
 
diff -r 53d8c91c86ec -r 31e08fe243f1 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/raw_simplifier.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -1385,7 +1385,7 @@
     Conv.fconv_rule
       (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th)
   |> Thm.adjust_maxidx_thm ~1
-  |> Drule.gen_all (Variable.maxidx_of ctxt);
+  |> Variable.gen_all ctxt;
 
 val hhf_ss =
   simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))
diff -r 53d8c91c86ec -r 31e08fe243f1 src/Pure/skip_proof.ML
--- a/src/Pure/skip_proof.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/skip_proof.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -38,6 +38,6 @@
 (* cheat_tac *)
 
 fun cheat_tac ctxt i st =
-  resolve_tac ctxt [make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))] i st;
+  resolve_tac ctxt [make_thm (Proof_Context.theory_of ctxt) (Var (("A", 0), propT))] i st;
 
 end;
diff -r 53d8c91c86ec -r 31e08fe243f1 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/thm.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -69,6 +69,7 @@
     tpairs: (cterm * cterm) list,
     prop: cterm}
   val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
+  val fold_atomic_cterms: (cterm -> 'a -> 'a) -> thm -> 'a -> 'a
   val terms_of_tpairs: (term * term) list -> term list
   val full_prop_of: thm -> term
   val theory_of_thm: thm -> theory
@@ -366,6 +367,15 @@
 fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) =
   fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps;
 
+fun fold_atomic_cterms f (th as Thm (_, {thy, maxidx, shyps, ...})) =
+  let fun cterm t T = Cterm {thy = thy, t = t, T = T, maxidx = maxidx, sorts = shyps} in
+    (fold_terms o fold_aterms)
+      (fn t as Const (_, T) => f (cterm t T)
+        | t as Free (_, T) => f (cterm t T)
+        | t as Var (_, T) => f (cterm t T)
+        | _ => I) th
+  end;
+
 fun terms_of_tpairs tpairs = fold_rev (fn (t, u) => cons t o cons u) tpairs [];
 
 fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u';
diff -r 53d8c91c86ec -r 31e08fe243f1 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/variable.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -59,6 +59,7 @@
   val fix_dummy_patterns: term -> Proof.context -> term * Proof.context
   val variant_fixes: string list -> Proof.context -> string list * Proof.context
   val dest_fixes: Proof.context -> (string * string) list
+  val gen_all: Proof.context -> thm -> thm
   val export_terms: Proof.context -> Proof.context -> term list -> term list
   val exportT_terms: Proof.context -> Proof.context -> term list -> term list
   val exportT: Proof.context -> Proof.context -> thm list -> thm list
@@ -497,6 +498,12 @@
 
 (** export -- generalize type/term variables (beware of closure sizes) **)
 
+fun gen_all ctxt th =
+  let
+    val i = Thm.maxidx_thm th (maxidx_of ctxt) + 1;
+    fun gen (x, T) = Thm.forall_elim (Thm.cterm_of ctxt (Var ((x, i), T)));
+  in fold gen (Drule.outer_params (Thm.prop_of th)) th end;
+
 fun export_inst inner outer =
   let
     val declared_outer = is_declared outer;
diff -r 53d8c91c86ec -r 31e08fe243f1 src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Sequents/simpdata.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -71,8 +71,7 @@
   setSSolver (mk_solver "safe" safe_solver)
   setSolver (mk_solver "unsafe" unsafe_solver)
   |> Simplifier.set_subgoaler asm_simp_tac
-  |> Simplifier.set_mksimps (fn ctxt =>
-      map (mk_meta_eq ctxt) o atomize o Drule.gen_all (Variable.maxidx_of ctxt))
+  |> Simplifier.set_mksimps (fn ctxt => map (mk_meta_eq ctxt) o atomize o Variable.gen_all ctxt)
   |> Simplifier.set_mkcong mk_meta_cong
   |> simpset_of;
 
diff -r 53d8c91c86ec -r 31e08fe243f1 src/ZF/Main_ZF.thy
--- a/src/ZF/Main_ZF.thy	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/ZF/Main_ZF.thy	Tue Jul 28 23:29:13 2015 +0200
@@ -72,7 +72,7 @@
 
 declaration \<open>fn _ =>
   Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
-    map mk_eq o Ord_atomize o Drule.gen_all (Variable.maxidx_of ctxt)))
+    map mk_eq o Ord_atomize o Variable.gen_all ctxt))
 \<close>
 
 end
diff -r 53d8c91c86ec -r 31e08fe243f1 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/ZF/OrdQuant.thy	Tue Jul 28 23:29:13 2015 +0200
@@ -362,7 +362,7 @@
 \<close>
 declaration \<open>fn _ =>
   Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
-    map mk_eq o Ord_atomize o Drule.gen_all (Variable.maxidx_of ctxt)))
+    map mk_eq o Ord_atomize o Variable.gen_all ctxt))
 \<close>
 
 text \<open>Setting up the one-point-rule simproc\<close>
diff -r 53d8c91c86ec -r 31e08fe243f1 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Tue Jul 28 23:29:13 2015 +0200
@@ -327,8 +327,7 @@
        If the premises get simplified, then the proofs could fail.*)
      val min_ss =
            (empty_simpset (Proof_Context.init_global thy)
-             |> Simplifier.set_mksimps (fn ctxt =>
-                 map mk_eq o ZF_atomize o Drule.gen_all (Variable.maxidx_of ctxt)))
+             |> Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt))
            setSolver (mk_solver "minimal"
                       (fn ctxt => resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt)
                                    ORELSE' assume_tac ctxt
diff -r 53d8c91c86ec -r 31e08fe243f1 src/ZF/pair.thy
--- a/src/ZF/pair.thy	Tue Jul 28 18:45:32 2015 +0200
+++ b/src/ZF/pair.thy	Tue Jul 28 23:29:13 2015 +0200
@@ -12,8 +12,7 @@
 
 setup \<open>
   map_theory_simpset
-    (Simplifier.set_mksimps (fn ctxt =>
-        map mk_eq o ZF_atomize o Drule.gen_all (Variable.maxidx_of ctxt))
+    (Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt)
       #> Simplifier.add_cong @{thm if_weak_cong})
 \<close>