inter_sort: keep normal!
authorwenzelm
Fri Jul 07 21:51:52 2000 +0200 (2000-07-07)
changeset 9281a48818595670
parent 9280 78a9bca983ac
child 9282 0181ac100520
inter_sort: keep normal!
src/Pure/sorts.ML
     1.1 --- a/src/Pure/sorts.ML	Fri Jul 07 18:29:34 2000 +0200
     1.2 +++ b/src/Pure/sorts.ML	Fri Jul 07 21:51:52 2000 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4    in intr S end;
     1.5  
     1.6  (*instersect sorts (preserves minimality)*)
     1.7 -fun inter_sort classrel = foldr (inter_class classrel);
     1.8 +fun inter_sort classrel = sort_strings o foldr (inter_class classrel);
     1.9  
    1.10  
    1.11