Now calls require_thy to ensure ancestors are present

--- 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 =