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