changeset 9281 | a48818595670 |
parent 7643 | 59f8feff9766 |
child 14782 | d6ce35a1c386 |
--- a/src/Pure/sorts.ML Fri Jul 07 18:29:34 2000 +0200 +++ b/src/Pure/sorts.ML Fri Jul 07 21:51:52 2000 +0200 @@ -130,7 +130,7 @@ in intr S end; (*instersect sorts (preserves minimality)*) -fun inter_sort classrel = foldr (inter_class classrel); +fun inter_sort classrel = sort_strings o foldr (inter_class classrel);