| changeset 18428 | 4059413acbc1 |
| parent 17756 | d4a35f82fbb4 |
| child 18931 | 427df66052a1 |
--- a/src/Pure/sorts.ML Sat Dec 17 01:00:38 2005 +0100 +++ b/src/Pure/sorts.ML Sat Dec 17 01:00:40 2005 +0100 @@ -140,7 +140,7 @@ fun norm_sort _ [] = [] | norm_sort _ (S as [_]) = S - | norm_sort classes S = unique_strings (sort_strings (filter (minimal_class classes S) S)); + | norm_sort classes S = sort_distinct string_ord (filter (minimal_class classes S) S); (* certify *)