src/Pure/drule.ML
changeset 2180 934572a94139
parent 2152 76d5ed939545
child 2266 82aef6857c5b
     1.1 --- a/src/Pure/drule.ML	Tue Nov 12 13:20:36 1996 +0100
     1.2 +++ b/src/Pure/drule.ML	Wed Nov 13 10:38:08 1996 +0100
     1.3 @@ -461,7 +461,7 @@
     1.4      let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
     1.5          and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
     1.6      in  Sign.eq_sg (sg1,sg2) andalso
     1.7 -        eq_set (shyps1, shyps2) andalso
     1.8 +        eq_set_sort (shyps1, shyps2) andalso
     1.9          aconvs(hyps1,hyps2) andalso
    1.10          prop1 aconv prop2
    1.11      end;
    1.12 @@ -473,7 +473,7 @@
    1.13      let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
    1.14          and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
    1.15      in  Sign.same_sg (sg1,sg2) andalso
    1.16 -        eq_set (shyps1, shyps2) andalso
    1.17 +        eq_set_sort (shyps1, shyps2) andalso
    1.18          aconvs(hyps1,hyps2) andalso
    1.19          prop1 aconv prop2
    1.20      end;