produce certified vars without access to theory_of_thm, and without context;

--- a/src/Pure/more_thm.ML	Sun Aug 16 19:44:21 2015 +0200
+++ b/src/Pure/more_thm.ML	Sun Aug 16 20:25:12 2015 +0200
@@ -314,28 +314,39 @@
 
 local
 
-fun forall_elim_vars_aux vars i th =
+fun dest_all ct =
+  (case Thm.term_of ct of
+    Const ("Pure.all", _) $ Abs (a, _, _) =>
+      let val (x, ct') = Thm.dest_abs NONE (Thm.dest_arg ct)
+      in SOME ((a, Thm.ctyp_of_cterm x), ct') end
+  | _ => NONE);
+
+fun dest_all_list ct =
+  (case dest_all ct of
+    NONE => []
+  | SOME (v, ct') => v :: dest_all_list ct');
+
+fun forall_elim_vars_list vars i th =
   let
-    val thy = Thm.theory_of_thm th;
     val used =
       (Thm.fold_terms o Term.fold_aterms)
         (fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I) th [];
-    val cvars = (Name.variant_list used (map #1 vars), vars)
-      |> ListPair.map (fn (x, (_, T)) => Thm.global_cterm_of thy (Var ((x, i), T)));
-  in fold Thm.forall_elim cvars th end;
+    val vars' = (Name.variant_list used (map #1 vars), vars)
+      |> ListPair.map (fn (x, (_, T)) => Thm.var ((x, i), T));
+  in fold Thm.forall_elim vars' th end;
 
 in
 
 fun forall_elim_vars i th =
-  forall_elim_vars_aux (Term.strip_all_vars (Thm.prop_of th)) i th;
+  forall_elim_vars_list (dest_all_list (Thm.cprop_of th)) i th;
 
 fun forall_elim_var i th =
   let
     val vars =
-      (case Thm.prop_of th of
-        Const ("Pure.all", _) $ Abs (a, T, _) => [(a, T)]
-      | _ => raise THM ("forall_elim_vars", i, [th]));
-  in forall_elim_vars_aux vars i th end;
+      (case dest_all (Thm.cprop_of th) of
+        SOME (v, _) => [v]
+      | NONE => raise THM ("forall_elim_var", i, [th]));
+  in forall_elim_vars_list vars i th end;
 
 end;
 

--- a/src/Pure/thm.ML	Sun Aug 16 19:44:21 2015 +0200
+++ b/src/Pure/thm.ML	Sun Aug 16 20:25:12 2015 +0200
@@ -40,6 +40,7 @@
   val dest_fun2: cterm -> cterm
   val dest_arg1: cterm -> cterm
   val dest_abs: string option -> cterm -> cterm * cterm
+  val var: indexname * ctyp -> cterm
   val apply: cterm -> cterm -> cterm
   val lambda_name: string * cterm -> cterm -> cterm
   val lambda: cterm -> cterm -> cterm
@@ -254,6 +255,10 @@
 
 (* constructors *)
 
+fun var ((x, i), Ctyp {thy, T, maxidx, sorts}) =
+  if i < 0 then raise TERM ("var: bad index", [Var ((x, i), T)])
+  else Cterm {thy = thy, t = Var ((x, i), T), T = T, maxidx = Int.max (i, maxidx), sorts = sorts};
+
 fun apply
   (cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...})
   (cx as Cterm {t = x, T, maxidx = maxidx2, sorts = sorts2, ...}) =