diff -r 4b605159b5a5 -r 019aadf0e315 src/ZF/add_ind_def.ML
--- a/src/ZF/add_ind_def.ML	Fri Nov 25 11:04:44 1994 +0100
+++ b/src/ZF/add_ind_def.ML	Fri Nov 25 11:08:12 1994 +0100
@@ -85,17 +85,19 @@
     val sign = sign_of thy;
 
     (*recT and rec_params should agree for all mutually recursive components*)
-    val (Const(_,recT),rec_params) = strip_comb (hd rec_tms)
-    and rec_hds = map head_of rec_tms;
+    val rec_hds = map head_of rec_tms;
 
-    val rec_names = map (#1 o dest_Const) rec_hds;
+    val _ = assert_all is_Const rec_hds
+	    (fn t => "Recursive set not previously declared as constant: " ^ 
+	             Sign.string_of_term sign t);
+
+    (*Now we know they are all Consts, so get their names, type and params*)
+    val rec_names = map (#1 o dest_Const) rec_hds
+    and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
 
     val _ = assert_all Syntax.is_identifier rec_names
        (fn a => "Name of recursive set not an identifier: " ^ a);
 
-    val _ = assert_all (is_some o Sign.const_type sign) rec_names
-       (fn a => "Recursive set not previously declared as constant: " ^ a);
-
     local (*Checking the introduction rules*)
       val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
       fun intr_ok set =