src/HOL/add_ind_def.ML

 
 
 (*Declares functions to add fixedpoint/constructor defs to a theory*)
 functor Add_inductive_def_Fun (Fp: FP) : ADD_INDUCTIVE_DEF =
 struct
-open Logic Ind_Syntax;
+open Ind_Syntax;
 
 (*internal version*)
 fun add_fp_def_i (rec_tms, intr_tms) thy = 
   let
     val sign = sign_of thy;

 
     (*Mutual recursion ?? *)
     val domTs = summands (dest_setT (body_type recT));
 	        (*alternative defn: map (dest_setT o fastype_of) rec_tms *)
     val dom_sumT = fold_bal mk_sum domTs;
-    val dom_set   = mk_setT dom_sumT;
+    val dom_set  = mk_setT dom_sumT;
 
     val freez   = Free(z, dom_sumT)
     and freeX   = Free(X, dom_set);
     (*type of w may be any of the domTs*)
 

       | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ 
 			      Sign.string_of_term sign Q);
 
     (*Makes a disjunct from an introduction rule*)
     fun lfp_part intr = (*quantify over rule's free vars except parameters*)
-      let val prems = map dest_tprop (strip_imp_prems intr)
+      let val prems = map dest_tprop (Logic.strip_imp_prems intr)
 	  val _ = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
 	  val exfrees = term_frees intr \\ rec_params
 	  val zeq = eq_const dom_sumT $ freez $ (#1 (rule_concl intr))
       in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
 

 
     val lfp_rhs = Fp.oper(X, dom_sumT, 
 			  mk_Collect(z, dom_sumT, 
 				     fold_bal (app disj) part_intrs))
 
-    val _ = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) 
-			       "Illegal occurrence of recursion operator")
-	     rec_hds;
 
     (*** Make the new theory ***)
 
     (*A key definition:
       If no mutual recursion then it equals the one recursive set.

 	     | _ => rec_tms ~~		(*define the sets as Parts*)
 		    map (subst_atomic [(freeX, big_rec_tm)]) parts));
 
     val _ = seq (writeln o Sign.string_of_term sign o #2) axpairs
   
+    (*Detect occurrences of operator, even with other types!*)
+    val _ = (case rec_names inter (add_term_names (lfp_rhs,[])) of
+	       [] => ()
+	     | x::_ => error ("Illegal occurrence of recursion op: " ^ x ^
+                               "\n\t*Consider adding type constraints*"))
+
   in  thy |> add_defs_i axpairs  end
 
 
 (****************************************************************OMITTED