# HG changeset patch
# User haftmann
# Date 1257774445 -3600
# Node ID 3ac7301d052fcc6930c39b6655cdc91db4e7ed74
# Parent  535789c26230f227233352df4abd4de57000e598# Parent  2c0a4adbcf133290252c907b540967f2c108b220
merged

diff -r 535789c26230 -r 3ac7301d052f src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Nov 09 11:34:22 2009 +0100
+++ b/src/Pure/Isar/code.ML	Mon Nov 09 14:47:25 2009 +0100
@@ -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