diff -r 018906568ef0 -r 934572a94139 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Nov 12 13:20:36 1996 +0100
+++ b/src/Pure/drule.ML	Wed Nov 13 10:38:08 1996 +0100
@@ -461,7 +461,7 @@
     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.eq_sg (sg1,sg2) andalso
-        eq_set (shyps1, shyps2) andalso
+        eq_set_sort (shyps1, shyps2) andalso
         aconvs(hyps1,hyps2) andalso
         prop1 aconv prop2
     end;
@@ -473,7 +473,7 @@
     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 (shyps1, shyps2) andalso
+        eq_set_sort (shyps1, shyps2) andalso
         aconvs(hyps1,hyps2) andalso
         prop1 aconv prop2
     end;