# HG changeset patch
# User wenzelm
# Date 880655768 -3600
# Node ID 03353197410c364a907241c42c6cde907e5d92d2
# Parent  63844406913c9b9ea50df1dc122bfc00fae4a1b2
removed same_thm;

diff -r 63844406913c -r 03353197410c src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Nov 27 14:05:25 1997 +0100
+++ b/src/Pure/drule.ML	Thu Nov 27 19:36:08 1997 +0100
@@ -42,7 +42,6 @@
   val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
   val read_instantiate	: (string*string)list -> thm -> thm
   val cterm_instantiate	: (cterm*cterm)list -> thm -> thm
-  val same_thm		: thm * thm -> bool
   val weak_eq_thm	: thm * thm -> bool
   val eq_thm_sg		: thm * thm -> bool
   val size_of_thm	: thm -> int
@@ -368,20 +367,6 @@
 
 (** theorem equality **)
 
-val eq_thm = Thm.eq_thm;
-
-(*equality of theorems using similarity of signatures,
-  i.e. the theorems belong to the same theory but not necessarily to the same
-  version of this theory*)
-fun same_thm (th1,th2) =
-    let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
-        and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
-    in  Sign.same_sg (sg1,sg2) andalso
-        eq_set_sort (shyps1, shyps2) andalso
-        aconvs(hyps1,hyps2) andalso
-        prop1 aconv prop2
-    end;
-
 (*Do the two theorems have the same signature?*)
 fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2));