src/Pure/sign.ML
changeset 18928 042608ffa2ec
parent 18892 51360da418b2
child 18941 18cb1e2ab77d
--- a/src/Pure/sign.ML	Mon Feb 06 11:00:24 2006 +0100
+++ b/src/Pure/sign.ML	Mon Feb 06 11:01:28 2006 +0100
@@ -628,7 +628,7 @@
 fun add_typedecls decls thy =
   let
     fun type_of (a, vs, mx) =
-      if null (duplicates vs) then (a, length vs, mx)
+      if not (has_duplicates (op =) vs) then (a, length vs, mx)
       else error ("Duplicate parameters in type declaration: " ^ quote a);
   in add_types (map type_of decls) thy end;