# HG changeset patch
# User wenzelm
# Date 1307645768 -7200
# Node ID c6bbeca3ee06d69c350fd6bd7b20ec357767f560
# Parent  84472e1985152189d8edfa5d0b85d67d1eb972db
clarified special incr_type_indexes;

diff -r 84472e198515 -r c6bbeca3ee06 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Jun 09 20:22:22 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Jun 09 20:56:08 2011 +0200
@@ -167,12 +167,19 @@
 
 (* INFERENCE RULE: RESOLVE *)
 
+(*Increment the indexes of only the type variables*)
+fun incr_type_indexes inc th =
+  let val tvs = Term.add_tvars (Thm.full_prop_of th) []
+      and thy = Thm.theory_of_thm th
+      fun inc_tvar ((a,i),s) = pairself (ctyp_of thy) (TVar ((a,i),s), TVar ((a,i+inc),s))
+  in Thm.instantiate (map inc_tvar tvs, []) th end;
+
 (* Like RSN, but we rename apart only the type variables. Vars here typically
    have an index of 1, and the use of RSN would increase this typically to 3.
    Instantiations of those Vars could then fail. *)
 fun resolve_inc_tyvars thy tha i thb =
   let
-    val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
+    val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
     fun aux tha thb =
       case Thm.bicompose false (false, tha, nprems_of tha) i thb
            |> Seq.list_of |> distinct Thm.eq_thm of
diff -r 84472e198515 -r c6bbeca3ee06 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Jun 09 20:22:22 2011 +0200
+++ b/src/Pure/drule.ML	Thu Jun 09 20:56:08 2011 +0200
@@ -110,7 +110,6 @@
   val comp_no_flatten: thm * int -> int -> thm -> thm
   val rename_bvars: (string * string) list -> thm -> thm
   val rename_bvars': string option list -> thm -> thm
-  val incr_type_indexes: int -> thm -> thm
   val incr_indexes: thm -> thm -> thm
   val incr_indexes2: thm -> thm -> thm -> thm
   val remdups_rl: thm
@@ -803,13 +802,6 @@
 
 (* var indexes *)
 
-(*Increment the indexes of only the type variables*)
-fun incr_type_indexes inc th =
-  let val tvs = OldTerm.term_tvars (prop_of th)
-      and thy = Thm.theory_of_thm th
-      fun inc_tvar ((a,i),s) = pairself (ctyp_of thy) (TVar ((a,i),s), TVar ((a,i+inc),s))
-  in Thm.instantiate (map inc_tvar tvs, []) th end;
-
 fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1);
 
 fun incr_indexes2 th1 th2 =