# HG changeset patch
# User paulson
# Date 859973267 -7200
# Node ID 7d640451ae7d0b1719f744bd1cacfb53c656165d
# Parent  1f3f5c44e159925da4716d7ba897659a70ebfb23
Now tests for essential ancestors (Lfp or Gfp)

diff -r 1f3f5c44e159 -r 7d640451ae7d src/HOL/add_ind_def.ML
--- 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*)