# HG changeset patch
# User lcp
# Date 806684596 -7200
# Node ID 563ecd14c1d8600443c61203452fa401a18fbd20
# Parent  026221bc9b2d17db2371589d52eeb428e4e9cf04
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)

diff -r 026221bc9b2d -r 563ecd14c1d8 src/Pure/drule.ML
--- 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 ***)