# HG changeset patch
# User oheimb
# Date 850912307 -3600
# Node ID b630fded45662f546c20b9f6382b59e1f5d1d65a
# Parent  63249c1c544a81784be5a5fc69e50e2f14f8dde9
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}

diff -r 63249c1c544a -r b630fded4566 src/Pure/Syntax/type_ext.ML
--- 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)))