Theory.require;
authorwenzelm
Wed, 29 Apr 1998 11:43:53 +0200 (1998-04-29)
changeset 4872 33e7cdc20681
parent 4871 fe076613e122
child 4873 b5999638979e
Theory.require;
src/HOL/Inductive.ML
--- 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