check for illegal merge of class parameters
authorhaftmann
Mon, 26 May 2008 17:55:36 +0200
changeset 26995 2511a72dd73c
parent 26994 197af793312c
child 26996 090a619e7d87
check for illegal merge of class parameters
src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon May 26 17:55:35 2008 +0200
+++ b/src/Pure/Isar/class.ML	Mon May 26 17:55:36 2008 +0200
@@ -469,6 +469,11 @@
     val supclasses = map (prep_class thy) raw_supclasses;
     val supsort = Sign.minimize_sort thy supclasses;
     val sups = filter (is_class thy) supsort;
+    val supparam_names = map fst (these_params thy sups);
+    val _ = if has_duplicates (op =) supparam_names
+      then error ("Duplicate parameter(s) in superclasses: "
+        ^ (commas o map quote o duplicates (op =)) supparam_names)
+      else ();
     val base_sort = if null sups then supsort else
       foldr1 (Sorts.inter_sort (Sign.classes_of thy))
         (map (#base_sort o the_class_data thy) sups);