# HG changeset patch
# User lcp
# Date 785758226 -3600
# Node ID 3f5136a61a72f114495ee5a1dab7df72be4a4c4e
# Parent  9e33eddca1221d75eca5dd4c4b0de0fa61f54d83
checks that the recursive sets are Consts before taking
them apart!  Bug was introduced during the translation to theory sections.

diff -r 9e33eddca122 -r 3f5136a61a72 add_ind_def.ML
--- a/add_ind_def.ML	Fri Nov 25 09:59:51 1994 +0100
+++ b/add_ind_def.ML	Fri Nov 25 11:10:26 1994 +0100
@@ -55,19 +55,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 domTs = summands(dest_set (body_type recT));
+    val _ = assert_all is_Const rec_hds
+	    (fn t => "Recursive set not previously declared as constant: " ^ 
+	             Sign.string_of_term sign t);
 
-    val rec_names = map (#1 o dest_Const) rec_hds;
+    (*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 =
@@ -87,6 +87,8 @@
 
     val z = mk_variant"z" and X = mk_variant"X" and w = mk_variant"w";
 
+    (*Probably INCORRECT for mutual recursion!*)
+    val domTs = summands(dest_set (body_type recT));
     val dom_sumT = fold_bal mk_sum domTs;
     val dom_set   = mk_set dom_sumT;