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