little improvement for the handling of sort constraints:
two non-identical explicit constriants are considered equal if they give
the same set in different enumerations, e.g. {term,ord,ord} = {ord,term}

--- a/src/Pure/Syntax/type_ext.ML	Wed Dec 18 12:47:28 1996 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Wed Dec 18 13:31:47 1996 +0100
@@ -49,7 +49,8 @@
 
     val env = distinct (env_of tm);
   in
-    (case gen_duplicates eq_fst env of
+    (case gen_duplicates 
+		(fn ((n,s),(m,t)) => n=m andalso not(eq_set_string(s,t))) env of
       [] => env
     | dups => error ("Inconsistent sort constraints for type variable(s) " ^
         commas (map (quote o show_var o #1) dups)))