better error messages for datatypes not declared Const

--- a/src/ZF/Tools/datatype_package.ML	Wed May 15 10:42:32 2002 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Wed May 15 10:44:58 2002 +0200
@@ -54,7 +54,13 @@
   val dummy = (*has essential ancestors?*)
     Theory.requires thy "Datatype" "(co)datatype definitions";
 
-  val rec_names = map (#1 o dest_Const o head_of) rec_tms
+  val rec_hds = map head_of rec_tms;
+
+  val dummy = assert_all is_Const rec_hds
+          (fn t => "Datatype set not previously declared as constant: " ^
+                   Sign.string_of_term (sign_of thy) t);
+
+  val rec_names = map (#1 o dest_Const) rec_hds
   val rec_base_names = map Sign.base_name rec_names
   val big_rec_base_name = space_implode "_" rec_base_names
 

--- a/src/ZF/ind_syntax.ML	Wed May 15 10:42:32 2002 +0200
+++ b/src/ZF/ind_syntax.ML	Wed May 15 10:44:58 2002 +0200
@@ -121,8 +121,12 @@
   definition other than Nat.nat and the datatype sets themselves.
   FIXME: could insert all constant set expressions, e.g. nat->nat.*)
 fun data_domain co (rec_tms, con_ty_lists) = 
-    let val rec_names = (*nat doesn't have to be added*)
-	    "Nat.nat" :: map (#1 o dest_Const o head_of) rec_tms
+    let val rec_hds = map head_of rec_tms
+        val dummy = assert_all is_Const rec_hds
+          (fn t => "Datatype set not previously declared as constant: " ^
+                   Sign.string_of_term (sign_of IFOL.thy) t);
+        val rec_names = (*nat doesn't have to be added*)
+	    "Nat.nat" :: map (#1 o dest_Const) rec_hds
 	val u = if co then quniv else univ
 	fun is_OK (Const(a,T)) = not (a mem_string rec_names)
 	  | is_OK _            = false