more explicit context;

--- a/src/FOL/simpdata.ML	Tue Jul 28 20:15:19 2015 +0200
+++ b/src/FOL/simpdata.ML	Tue Jul 28 20:59:39 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 **)

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Jul 28 20:15:19 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Jul 28 20:59:39 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)))));

--- a/src/HOL/Tools/simpdata.ML	Tue Jul 28 20:15:19 2015 +0200
+++ b/src/HOL/Tools/simpdata.ML	Tue Jul 28 20:59:39 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

--- a/src/Pure/Isar/local_defs.ML	Tue Jul 28 20:15:19 2015 +0200
+++ b/src/Pure/Isar/local_defs.ML	Tue Jul 28 20:59:39 2015 +0200
@@ -131,6 +131,8 @@
 *)
 fun export inner outer =    (*beware of closure sizes*)
   let
+    val thy = Proof_Context.theory_of inner;
+    val maxidx0 = Variable.maxidx_of outer;
     val exp = Assumption.export false inner outer;
     val exp_term = Assumption.export_term inner outer;
     val asms = Assumption.local_assms_of inner outer;
@@ -149,7 +151,7 @@
                     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))
+                      else (Drule.abs_def (Drule.gen_all thy maxidx0 asm), true))
                 end)));
       in (apply2 (map #1) (List.partition #2 defs_asms), th') end
   end;

--- a/src/Pure/Isar/object_logic.ML	Tue Jul 28 20:15:19 2015 +0200
+++ b/src/Pure/Isar/object_logic.ML	Tue Jul 28 20:59:39 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;
 

--- a/src/Pure/drule.ML	Tue Jul 28 20:15:19 2015 +0200
+++ b/src/Pure/drule.ML	Tue Jul 28 20:59:39 2015 +0200
@@ -16,7 +16,7 @@
   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 gen_all: theory -> 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
@@ -183,9 +183,8 @@
   in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end;
 
 (*generalize outermost parameters*)
-fun gen_all maxidx0 th =
+fun gen_all thy 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) =

--- a/src/Pure/raw_simplifier.ML	Tue Jul 28 20:15:19 2015 +0200
+++ b/src/Pure/raw_simplifier.ML	Tue Jul 28 20:59:39 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 ()))

--- a/src/Pure/variable.ML	Tue Jul 28 20:15:19 2015 +0200
+++ b/src/Pure/variable.ML	Tue Jul 28 20:59:39 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,8 @@
 
 (** export -- generalize type/term variables (beware of closure sizes) **)
 
+fun gen_all ctxt = Drule.gen_all (Proof_Context.theory_of ctxt) (maxidx_of ctxt);
+
 fun export_inst inner outer =
   let
     val declared_outer = is_declared outer;

--- a/src/Sequents/simpdata.ML	Tue Jul 28 20:15:19 2015 +0200
+++ b/src/Sequents/simpdata.ML	Tue Jul 28 20:59:39 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;
 

--- a/src/ZF/Main_ZF.thy	Tue Jul 28 20:15:19 2015 +0200
+++ b/src/ZF/Main_ZF.thy	Tue Jul 28 20:59:39 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

--- a/src/ZF/OrdQuant.thy	Tue Jul 28 20:15:19 2015 +0200
+++ b/src/ZF/OrdQuant.thy	Tue Jul 28 20:59:39 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>

--- a/src/ZF/Tools/inductive_package.ML	Tue Jul 28 20:15:19 2015 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Tue Jul 28 20:59:39 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

--- a/src/ZF/pair.thy	Tue Jul 28 20:15:19 2015 +0200
+++ b/src/ZF/pair.thy	Tue Jul 28 20:59:39 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>