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 =