# HG changeset patch
# User wenzelm
# Date 1439754911 -7200
# Node ID 762cb38a314723a4df34f1682a3cb7815239c816
# Parent  b70c4db3874f733ee58ceba778ec7908db5394fe
produce certified vars without access to theory_of_thm, and without context;

diff -r b70c4db3874f -r 762cb38a3147 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sun Aug 16 20:25:12 2015 +0200
+++ b/src/Pure/drule.ML	Sun Aug 16 21:55:11 2015 +0200
@@ -219,12 +219,16 @@
 fun zero_var_indexes_list [] = []
   | zero_var_indexes_list ths =
       let
-        val thy = Theory.merge_list (map Thm.theory_of_thm ths);
         val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
-        val insts' =
-         (map (apsnd (Thm.global_ctyp_of thy)) instT,
-          map (apsnd (Thm.global_cterm_of thy)) inst);
-      in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate insts') ths end;
+
+        val tvars = fold Thm.add_tvars ths [];
+        fun the_tvar v = the (find_first (fn cT => v = dest_TVar (Thm.typ_of cT)) tvars);
+        val instT' = map (fn (v, TVar (b, _)) => (v, Thm.rename_tvar b (the_tvar v))) instT;
+
+        val vars = fold (Thm.add_vars o Thm.instantiate (instT', [])) ths [];
+        fun the_var v = the (find_first (fn ct => v = dest_Var (Thm.term_of ct)) vars);
+        val inst' = map (fn (v, Var (b, _)) => (v, Thm.var (b, Thm.ctyp_of_cterm (the_var v)))) inst;
+      in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (instT', inst')) ths end;
 
 val zero_var_indexes = singleton zero_var_indexes_list;
 
diff -r b70c4db3874f -r 762cb38a3147 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sun Aug 16 20:25:12 2015 +0200
+++ b/src/Pure/more_thm.ML	Sun Aug 16 21:55:11 2015 +0200
@@ -20,7 +20,9 @@
   include THM
   structure Ctermtab: TABLE
   structure Thmtab: TABLE
+  val eq_ctyp: ctyp * ctyp -> bool
   val aconvc: cterm * cterm -> bool
+  val add_tvars: thm -> ctyp list -> ctyp list
   val add_frees: thm -> cterm list -> cterm list
   val add_vars: thm -> cterm list -> cterm list
   val all_name: Proof.context -> string * cterm -> cterm -> cterm
@@ -110,10 +112,12 @@
 
 (** basic operations **)
 
-(* collecting cterms *)
+(* collecting ctyps and cterms *)
 
+val eq_ctyp = op = o apply2 Thm.typ_of;
 val op aconvc = op aconv o apply2 Thm.term_of;
 
+val add_tvars = Thm.fold_atomic_ctyps (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a);
 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);
 
diff -r b70c4db3874f -r 762cb38a3147 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Aug 16 20:25:12 2015 +0200
+++ b/src/Pure/thm.ML	Sun Aug 16 21:55:11 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 rename_tvar: indexname -> ctyp -> ctyp
   val var: indexname * ctyp -> cterm
   val apply: cterm -> cterm -> cterm
   val lambda_name: string * cterm -> cterm -> cterm
@@ -60,6 +61,7 @@
     tpairs: (term * term) list,
     prop: term}
   val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
+  val fold_atomic_ctyps: (ctyp -> '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
@@ -255,6 +257,16 @@
 
 (* constructors *)
 
+fun rename_tvar (a, i) (Ctyp {thy, T, maxidx, sorts}) =
+  let
+    val S =
+      (case T of
+        TFree (_, S) => S
+      | TVar (_, S) => S
+      | _ => raise TYPE ("rename_tvar: no variable", [T], []));
+    val _ = if i < 0 then raise TYPE ("rename_tvar: bad index", [TVar ((a, i), S)], []) else ();
+  in Ctyp {thy = thy, T = TVar ((a, i), S), maxidx = Int.max (i, maxidx), sorts = sorts} end;
+
 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};
@@ -354,6 +366,10 @@
 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_ctyps f (th as Thm (_, {thy, maxidx, shyps, ...})) =
+  let fun ctyp T = Ctyp {thy = thy, T = T, maxidx = maxidx, sorts = shyps}
+  in (fold_terms o fold_types o fold_atyps) (f o ctyp) th end;
+
 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)