--- 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
--- 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 =