merged
authorpaulson
Mon, 09 Nov 2009 15:50:31 +0000
changeset 33534 b21c820dfb63
parent 33532 3ac7301d052f (diff)
parent 33533 40b44cb20c8c (current diff)
child 33535 b233f48a4d3d
merged
--- a/src/Pure/Isar/code.ML	Mon Nov 09 15:50:15 2009 +0000
+++ b/src/Pure/Isar/code.ML	Mon Nov 09 15:50:31 2009 +0000
@@ -343,15 +343,17 @@
   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 no_constr s (c, ty) = error ("Not a datatype constructor:\n" ^ string_of_const thy c
+      ^ " :: " ^ string_of_typ thy ty ^ "\n" ^ enclose "(" ")" s);
     fun last_typ c_ty ty =
       let
-        val frees = OldTerm.typ_tfrees ty;
+        val tfrees = Term.add_tfreesT ty [];
         val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty
-          handle TYPE _ => no_constr c_ty
-        val _ = if has_duplicates (eq_fst (op =)) vs then no_constr c_ty else ();
-        val _ = if length frees <> length vs then no_constr c_ty else ();
+          handle TYPE _ => no_constr "bad type" c_ty
+        val _ = if has_duplicates (eq_fst (op =)) vs
+          then no_constr "duplicate type variables in datatype" c_ty else ();
+        val _ = if length tfrees <> length vs
+          then no_constr "type variables missing in datatype" c_ty else ();
       in (tyco, vs) end;
     fun ty_sorts (c, ty) =
       let