# HG changeset patch
# User paulson
# Date 1021452298 -7200
# Node ID 0c50d13d449a27d3be2dd914e39e32fd4ef09bde
# Parent  773657d466cba07acb70511cf4b2613d590c4dea
better error messages for datatypes not declared Const

diff -r 773657d466cb -r 0c50d13d449a src/ZF/Tools/datatype_package.ML
--- 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
 
diff -r 773657d466cb -r 0c50d13d449a src/ZF/ind_syntax.ML
--- 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