# HG changeset patch
# User wenzelm
# Date 924266564 -7200
# Node ID 154b88d2b62eaa18dcacba9153f738b1e8a06eeb
# Parent  f2a2a40e56c826126ca4a81a14cb5668ea05e21d
added incr_indexes, incr_indexes_wrt;

diff -r f2a2a40e56c8 -r 154b88d2b62e src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Apr 15 18:10:49 1999 +0200
+++ b/src/Pure/drule.ML	Fri Apr 16 14:42:44 1999 +0200
@@ -74,6 +74,8 @@
   val swap_prems_rl     : thm
   val equal_intr_rule   : thm
   val instantiate'	: ctyp option list -> cterm option list -> thm -> thm
+  val incr_indexes	: int -> thm -> thm
+  val incr_indexes_wrt	: int list -> ctyp list -> cterm list -> thm list -> thm -> thm
 end;
 
 signature DRULE =
@@ -669,6 +671,27 @@
   in instantiate' [] frees thm end;
 
 
+(* increment var indexes *)
+
+fun incr_indexes 0 thm = thm
+  | incr_indexes inc thm =
+      let
+        val sign = Thm.sign_of_thm thm;
+
+        fun inc_tvar ((x, i), S) = Some (Thm.ctyp_of sign (TVar ((x, i + inc), S)));
+        fun inc_var ((x, i), T) = Some (Thm.cterm_of sign (Var ((x, i + inc), T)));
+      in instantiate' (map inc_tvar (tvars_of thm)) (map inc_var (vars_of thm)) thm end;
+
+fun incr_indexes_wrt is cTs cts thms =
+  let
+    val maxidx =
+      foldl Int.max (~1, is @
+        map (maxidx_of_typ o #T o Thm.rep_ctyp) cTs @
+        map (#maxidx o Thm.rep_cterm) cts @
+        map (#maxidx o Thm.rep_thm) thms);
+  in incr_indexes (maxidx + 1) end;
+
+
 (* mk_triv_goal *)
 
 (*make an initial proof state, "PROP A ==> (PROP A)" *)