# HG changeset patch
# User paulson
# Date 859972600 -7200
# Node ID 36f75c4a0047e5e8273b2312700383105421f646
# Parent  f03b1652fc6a49ac69bd098ada4eec84d111aa30
Now calls require_thy to ensure ancestors are present

diff -r f03b1652fc6a -r 36f75c4a0047 src/HOL/Inductive.ML
--- a/src/HOL/Inductive.ML	Wed Apr 02 11:15:46 1997 +0200
+++ b/src/HOL/Inductive.ML	Wed Apr 02 11:16:40 1997 +0200
@@ -18,6 +18,7 @@
 
 structure Lfp_items =
   struct
+  val checkThy	= (fn thy => require_thy thy "Lfp" "inductive definitions")
   val oper      = gen_fp_oper "lfp"
   val Tarski    = def_lfp_Tarski
   val induct    = def_induct
@@ -25,6 +26,7 @@
 
 structure Gfp_items =
   struct
+  val checkThy	= (fn thy => require_thy thy "Gfp" "coinductive definitions")
   val oper      = gen_fp_oper "gfp"
   val Tarski    = def_gfp_Tarski
   val induct    = def_Collect_coinduct
@@ -63,7 +65,7 @@
   end;
 
 
-(*For upwards compatibility: can be called directly from ML*)
+(*Called by the theory sections or directly from ML*)
 functor Inductive_Fun
  (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end)
    : sig include INTR_ELIM INDRULE end =