--- 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));