Changed require to requires for MLWorks
authorpaulson
Wed May 27 12:21:39 1998 +0200 (1998-05-27)
changeset 49708b65444edbb0
parent 4969 61fd5c1d733f
child 4971 09b8945cac07
Changed require to requires for MLWorks
TFL/post.sml
src/HOL/Inductive.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/typedef_package.ML
src/HOL/datatype.ML
src/Pure/theory.ML
src/ZF/add_ind_def.ML
     1.1 --- a/TFL/post.sml	Wed May 27 12:19:35 1998 +0200
     1.2 +++ b/TFL/post.sml	Wed May 27 12:21:39 1998 +0200
     1.3 @@ -84,7 +84,7 @@
     1.4   * Defining a function with an associated termination relation. 
     1.5   *---------------------------------------------------------------------------*)
     1.6  fun define_i thy fid R eqs = 
     1.7 -  let val dummy = Theory.require thy "WF_Rel" "recursive function definitions"
     1.8 +  let val dummy = Theory.requires thy "WF_Rel" "recursive function definitions"
     1.9        val {functional,pats} = Prim.mk_functional thy eqs
    1.10    in (Prim.wfrec_definition0 thy fid R functional, pats)
    1.11    end;
     2.1 --- a/src/HOL/Inductive.ML	Wed May 27 12:19:35 1998 +0200
     2.2 +++ b/src/HOL/Inductive.ML	Wed May 27 12:21:39 1998 +0200
     2.3 @@ -18,7 +18,7 @@
     2.4  
     2.5  structure Lfp_items =
     2.6    struct
     2.7 -  val checkThy	= (fn thy => Theory.require thy "Lfp" "inductive definitions")
     2.8 +  val checkThy	= (fn thy => Theory.requires thy "Lfp" "inductive definitions")
     2.9    val oper      = gen_fp_oper "lfp"
    2.10    val Tarski    = def_lfp_Tarski
    2.11    val induct    = def_induct
    2.12 @@ -26,7 +26,7 @@
    2.13  
    2.14  structure Gfp_items =
    2.15    struct
    2.16 -  val checkThy	= (fn thy => Theory.require thy "Gfp" "coinductive definitions")
    2.17 +  val checkThy	= (fn thy => Theory.requires thy "Gfp" "coinductive definitions")
    2.18    val oper      = gen_fp_oper "gfp"
    2.19    val Tarski    = def_gfp_Tarski
    2.20    val induct    = def_Collect_coinduct
     3.1 --- a/src/HOL/Tools/record_package.ML	Wed May 27 12:19:35 1998 +0200
     3.2 +++ b/src/HOL/Tools/record_package.ML	Wed May 27 12:21:39 1998 +0200
     3.3 @@ -621,7 +621,7 @@
     3.4  
     3.5  fun gen_add_record prep_typ prep_raw_parent (params, bname) raw_parent raw_fields thy =
     3.6    let
     3.7 -    val _ = Theory.require thy "Record" "record definitions";
     3.8 +    val _ = Theory.requires thy "Record" "record definitions";
     3.9      val sign = Theory.sign_of thy;
    3.10      val _ = writeln ("Defining record " ^ quote bname ^ " ...");
    3.11  
     4.1 --- a/src/HOL/Tools/typedef_package.ML	Wed May 27 12:19:35 1998 +0200
     4.2 +++ b/src/HOL/Tools/typedef_package.ML	Wed May 27 12:21:39 1998 +0200
     4.3 @@ -43,7 +43,7 @@
     4.4  
     4.5  fun gen_add_typedef prep_term name (t, vs, mx) raw_set axms thms usr_tac thy =
     4.6    let
     4.7 -    val _ = Theory.require thy "Set" "typedefs";
     4.8 +    val _ = Theory.requires thy "Set" "typedefs";
     4.9      val sign = sign_of thy;
    4.10      val full_name = Sign.full_name sign;
    4.11  
     5.1 --- a/src/HOL/datatype.ML	Wed May 27 12:19:35 1998 +0200
     5.2 +++ b/src/HOL/datatype.ML	Wed May 27 12:21:39 1998 +0200
     5.3 @@ -209,7 +209,7 @@
     5.4  in
     5.5    fun add_datatype (typevars, tname, cons_list') thy = 
     5.6      let
     5.7 -      val dummy = Theory.require thy "Arith" "datatype definitions";
     5.8 +      val dummy = Theory.requires thy "Arith" "datatype definitions";
     5.9        
    5.10        fun typid(dtRek(_,id)) = id
    5.11          | typid(dtVar s) = implode (tl (explode s))
     6.1 --- a/src/Pure/theory.ML	Wed May 27 12:19:35 1998 +0200
     6.2 +++ b/src/Pure/theory.ML	Wed May 27 12:21:39 1998 +0200
     6.3 @@ -84,7 +84,7 @@
     6.4    val put_data: string * object -> theory -> theory
     6.5    val prep_ext: theory -> theory
     6.6    val prep_ext_merge: theory list -> theory
     6.7 -  val require: theory -> string -> string -> unit
     6.8 +  val requires: theory -> string -> string -> unit
     6.9    val pre_pure: theory
    6.10  end;
    6.11  
    6.12 @@ -125,7 +125,7 @@
    6.13  val eq_thy = Sign.eq_sg o pairself sign_of;
    6.14  
    6.15  (*check for some named theory*)
    6.16 -fun require thy name what =
    6.17 +fun requires thy name what =
    6.18    if exists (equal name) (Sign.stamp_names_of (sign_of thy)) then ()
    6.19    else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
    6.20  
     7.1 --- a/src/ZF/add_ind_def.ML	Wed May 27 12:19:35 1998 +0200
     7.2 +++ b/src/ZF/add_ind_def.ML	Wed May 27 12:21:39 1998 +0200
     7.3 @@ -72,7 +72,7 @@
     7.4  fun add_fp_def_i (rec_tms, dom_sum, intr_tms) thy = 
     7.5    let
     7.6      val dummy = (*has essential ancestors?*)
     7.7 -	Theory.require thy "Inductive" "(co)inductive definitions" 
     7.8 +	Theory.requires thy "Inductive" "(co)inductive definitions" 
     7.9  
    7.10      val sign = sign_of thy;
    7.11  
    7.12 @@ -178,7 +178,7 @@
    7.13  fun add_constructs_def (rec_base_names, con_ty_lists) thy = 
    7.14    let
    7.15      val dummy = (*has essential ancestors?*)
    7.16 -      Theory.require thy "Datatype" "(co)datatype definitions";
    7.17 +      Theory.requires thy "Datatype" "(co)datatype definitions";
    7.18  
    7.19      val sign = sign_of thy;
    7.20      val full_name = Sign.full_name sign;