# HG changeset patch
# User haftmann
# Date 1211817336 -7200
# Node ID 2511a72dd73cbb301f5416881ac81ba8795cf38e
# Parent  197af793312c145e8bf5c34932b4a7970695f897
check for illegal merge of class parameters

diff -r 197af793312c -r 2511a72dd73c 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);