--- 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)" *)