# HG changeset patch
# User haftmann
# Date 1225209540 -3600
# Node ID 8703d17c5e68c97cad97e91f340ce5a4073b815a
# Parent  aef727ef30e5d8bdadbca5151d627071d693e105
assert that no class parameter is used as constructor

diff -r aef727ef30e5 -r 8703d17c5e68 src/Pure/Isar/code_unit.ML
--- a/src/Pure/Isar/code_unit.ML	Tue Oct 28 16:58:59 2008 +0100
+++ b/src/Pure/Isar/code_unit.ML	Tue Oct 28 16:59:00 2008 +0100
@@ -280,6 +280,8 @@
 
 fun constrset_of_consts thy cs =
   let
+    val _ = map (fn (c, _) => if (is_some o AxClass.class_of_param thy) c
+      then error ("Is a class parameter: " ^ string_of_const thy c) else ()) cs;
     fun no_constr (c, ty) = error ("Not a datatype constructor: " ^ string_of_const thy c
       ^ " :: " ^ string_of_typ thy ty);
     fun last_typ c_ty ty =