# HG changeset patch
# User paulson
# Date 1187957874 -7200
# Node ID d89e409cfe4e3f2cb4ae91087885180d6627c0a8
# Parent  ca97c6f3d9cdf97e6e1b7d4dbee101f4d1c2e752
new derived rule: incr_type_indexes

diff -r ca97c6f3d9cd -r d89e409cfe4e src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Aug 24 14:16:44 2007 +0200
+++ b/src/Pure/drule.ML	Fri Aug 24 14:17:54 2007 +0200
@@ -121,6 +121,7 @@
   val with_subgoal: int -> (thm -> thm) -> 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
@@ -495,16 +496,16 @@
   with no lifting or renaming!  Q may contain ==> or meta-quants
   ALWAYS deletes premise i *)
 fun compose(tha,i,thb) =
-    Seq.list_of (bicompose false (false,tha,0) i thb);
+    distinct Thm.eq_thm (Seq.list_of (bicompose false (false,tha,0) i thb));
 
 fun compose_single (tha,i,thb) =
-  (case compose (tha,i,thb) of
+  case compose (tha,i,thb) of
     [th] => th
-  | _ => raise THM ("compose: unique result expected", i, [tha,thb]));
+  | _ => raise THM ("compose: unique result expected", i, [tha,thb]);
 
 (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
 fun tha COMP thb =
-    case distinct Thm.eq_thm (compose(tha,1,thb)) of
+    case compose(tha,1,thb) of
         [th] => th
       | _ =>   raise THM("COMP", 1, [tha,thb]);
 
@@ -764,6 +765,13 @@
 
 (* var indexes *)
 
+(*Increment the indexes of only the type variables*)
+fun incr_type_indexes inc th =
+  let val tvs = term_tvars (prop_of th)
+      and thy = 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 =