--- a/src/HOL/Inductive.ML Wed Apr 29 11:43:34 1998 +0200
+++ b/src/HOL/Inductive.ML Wed Apr 29 11:43:53 1998 +0200
@@ -18,7 +18,7 @@
structure Lfp_items =
struct
- val checkThy = (fn thy => require_thy thy "Lfp" "inductive definitions")
+ val checkThy = (fn thy => Theory.require thy "Lfp" "inductive definitions")
val oper = gen_fp_oper "lfp"
val Tarski = def_lfp_Tarski
val induct = def_induct
@@ -26,7 +26,7 @@
structure Gfp_items =
struct
- val checkThy = (fn thy => require_thy thy "Gfp" "coinductive definitions")
+ val checkThy = (fn thy => Theory.require thy "Gfp" "coinductive definitions")
val oper = gen_fp_oper "gfp"
val Tarski = def_gfp_Tarski
val induct = def_Collect_coinduct