src/Pure/drule.ML
 changeset 4313 03353197410c parent 4285 05af145a61d4 child 4440 9ed4098074bc
```     1.1 --- a/src/Pure/drule.ML	Thu Nov 27 14:05:25 1997 +0100
1.2 +++ b/src/Pure/drule.ML	Thu Nov 27 19:36:08 1997 +0100
1.3 @@ -42,7 +42,6 @@
1.4    val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
1.5    val read_instantiate	: (string*string)list -> thm -> thm
1.6    val cterm_instantiate	: (cterm*cterm)list -> thm -> thm
1.7 -  val same_thm		: thm * thm -> bool
1.8    val weak_eq_thm	: thm * thm -> bool
1.9    val eq_thm_sg		: thm * thm -> bool
1.10    val size_of_thm	: thm -> int
1.11 @@ -368,20 +367,6 @@
1.12
1.13  (** theorem equality **)
1.14
1.15 -val eq_thm = Thm.eq_thm;
1.16 -
1.17 -(*equality of theorems using similarity of signatures,
1.18 -  i.e. the theorems belong to the same theory but not necessarily to the same
1.19 -  version of this theory*)
1.20 -fun same_thm (th1,th2) =
1.21 -    let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
1.22 -        and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
1.23 -    in  Sign.same_sg (sg1,sg2) andalso
1.24 -        eq_set_sort (shyps1, shyps2) andalso
1.25 -        aconvs(hyps1,hyps2) andalso
1.26 -        prop1 aconv prop2
1.27 -    end;
1.28 -
1.29  (*Do the two theorems have the same signature?*)
1.30  fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2));
1.31
```