1.1 --- a/src/HOL/Inductive.ML	Wed Apr 29 11:43:34 1998 +0200
     1.2 +++ b/src/HOL/Inductive.ML	Wed Apr 29 11:43:53 1998 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  
     1.5  structure Lfp_items =
     1.6    struct
     1.7 -  val checkThy	= (fn thy => require_thy thy "Lfp" "inductive definitions")
     1.8 +  val checkThy	= (fn thy => Theory.require thy "Lfp" "inductive definitions")
     1.9    val oper      = gen_fp_oper "lfp"
    1.10    val Tarski    = def_lfp_Tarski
    1.11    val induct    = def_induct
    1.12 @@ -26,7 +26,7 @@
    1.13  
    1.14  structure Gfp_items =
    1.15    struct
    1.16 -  val checkThy	= (fn thy => require_thy thy "Gfp" "coinductive definitions")
    1.17 +  val checkThy	= (fn thy => Theory.require thy "Gfp" "coinductive definitions")
    1.18    val oper      = gen_fp_oper "gfp"
    1.19    val Tarski    = def_gfp_Tarski
    1.20    val induct    = def_Collect_coinduct