Improved error message, suggesting addition of
type constraints if occurrences of the recursive set remain in the
fixedpoint definition.
--- a/src/HOL/add_ind_def.ML Fri Dec 08 11:17:05 1995 +0100
+++ b/src/HOL/add_ind_def.ML Fri Dec 08 11:40:42 1995 +0100
@@ -47,7 +47,7 @@
(*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 =
@@ -91,7 +91,7 @@
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);
@@ -103,7 +103,7 @@
(*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))
@@ -129,9 +129,6 @@
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 ***)
@@ -153,6 +150,12 @@
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