--- a/src/Pure/drule.ML Tue Jul 25 17:02:34 1995 +0200
+++ b/src/Pure/drule.ML Tue Jul 25 17:03:16 1995 +0200
@@ -30,6 +30,7 @@
val flexpair_abs_elim_list: cterm list -> thm -> thm
val forall_intr_list : cterm list -> thm -> thm
val forall_intr_frees : thm -> thm
+ val forall_intr_vars : thm -> thm
val forall_elim_list : cterm list -> thm -> thm
val forall_elim_var : int -> thm -> thm
val forall_elim_vars : int -> thm -> thm
@@ -644,6 +645,27 @@
val size_of_thm = size_of_term o #prop o rep_thm;
+(** Mark Staples's weaker version of eq_thm: ignores variable renaming and
+ (some) type variable renaming **)
+
+ (* Can't use term_vars, because it sorts the resulting list of variable names.
+ We instead need the unique list noramlised by the order of appearance
+ in the term. *)
+fun term_vars' (t as Var(v,T)) = [t]
+ | term_vars' (Abs(_,_,b)) = term_vars' b
+ | term_vars' (f$a) = (term_vars' f) @ (term_vars' a)
+ | term_vars' _ = [];
+
+fun forall_intr_vars th =
+ let val {prop,sign,...} = rep_thm th;
+ val vars = distinct (term_vars' prop);
+ in forall_intr_list (map (cterm_of sign) vars) th end;
+
+fun weak_eq_thm (tha,thb) =
+ eq_thm(forall_intr_vars (freezeT tha), forall_intr_vars (freezeT thb));
+
+
+
(*** Meta-Rewriting Rules ***)