changeset 2438 | b630fded4566 |
parent 1511 | 09354d37a5ab |
child 2584 | b386951e15e6 |
--- 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)))