--- a/src/HOL/add_ind_def.ML Wed Apr 02 11:25:04 1997 +0200
+++ b/src/HOL/add_ind_def.ML Wed Apr 02 11:27:47 1997 +0200
@@ -31,9 +31,10 @@
signature FP = (** Description of a fixed point operator **)
sig
+ val checkThy : theory -> unit (*signals error if Lfp/Gfp is missing*)
val oper : string * typ * term -> term (*fixed point operator*)
- val Tarski : thm (*Tarski's fixed point theorem*)
- val induct : thm (*induction/coinduction rule*)
+ val Tarski : thm (*Tarski's fixed point theorem*)
+ val induct : thm (*induction/coinduction rule*)
end;
@@ -52,6 +53,8 @@
(*internal version*)
fun add_fp_def_i (rec_tms, intr_tms) thy =
let
+ val dummy = Fp.checkThy thy (*has essential ancestors?*)
+
val sign = sign_of thy;
(*rec_params should agree for all mutually recursive components*)