--- 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