src/Pure/sorts.ML
changeset 23585 f07ef41ffb87
parent 22570 f166a5416b3f
child 23655 d2d1138e0ddc
     1.1 --- a/src/Pure/sorts.ML	Thu Jul 05 00:06:23 2007 +0200
     1.2 +++ b/src/Pure/sorts.ML	Thu Jul 05 00:06:24 2007 +0200
     1.3 @@ -136,7 +136,7 @@
     1.4  (* sort relations *)
     1.5  
     1.6  fun sort_le algebra (S1, S2) =
     1.7 -  forall (fn c2 => exists (fn c1 => class_le algebra (c1, c2)) S1) S2;
     1.8 +  S1 = S2 orelse forall (fn c2 => exists (fn c1 => class_le algebra (c1, c2)) S1) S2;
     1.9  
    1.10  fun sorts_le algebra (Ss1, Ss2) =
    1.11    ListPair.all (sort_le algebra) (Ss1, Ss2);