# HG changeset patch
# User wenzelm
# Date 893843033 -7200
# Node ID 33e7cdc20681ef5418501e5079a40422700d284d
# Parent  fe076613e1228e5b9ff75fbaebe5520367be4bc2
Theory.require;

diff -r fe076613e122 -r 33e7cdc20681 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