assert that no class parameter is used as constructor
authorhaftmann
Tue, 28 Oct 2008 16:59:00 +0100
changeset 28704 8703d17c5e68
parent 28703 aef727ef30e5
child 28705 c77a9f5672f8
assert that no class parameter is used as constructor
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 =