# HG changeset patch
# User paulson
# Date 896264499 -7200
# Node ID 8b65444edbb00a167f19a962df405dfaf891f2b4
# Parent  61fd5c1d733f83fe4e451b16c37099b4838eaedb
Changed require to requires for MLWorks

diff -r 61fd5c1d733f -r 8b65444edbb0 TFL/post.sml
--- a/TFL/post.sml	Wed May 27 12:19:35 1998 +0200
+++ b/TFL/post.sml	Wed May 27 12:21:39 1998 +0200
@@ -84,7 +84,7 @@
  * Defining a function with an associated termination relation. 
  *---------------------------------------------------------------------------*)
 fun define_i thy fid R eqs = 
-  let val dummy = Theory.require thy "WF_Rel" "recursive function definitions"
+  let val dummy = Theory.requires thy "WF_Rel" "recursive function definitions"
       val {functional,pats} = Prim.mk_functional thy eqs
   in (Prim.wfrec_definition0 thy fid R functional, pats)
   end;
diff -r 61fd5c1d733f -r 8b65444edbb0 src/HOL/Inductive.ML
--- a/src/HOL/Inductive.ML	Wed May 27 12:19:35 1998 +0200
+++ b/src/HOL/Inductive.ML	Wed May 27 12:21:39 1998 +0200
@@ -18,7 +18,7 @@
 
 structure Lfp_items =
   struct
-  val checkThy	= (fn thy => Theory.require thy "Lfp" "inductive definitions")
+  val checkThy	= (fn thy => Theory.requires 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 => Theory.require thy "Gfp" "coinductive definitions")
+  val checkThy	= (fn thy => Theory.requires thy "Gfp" "coinductive definitions")
   val oper      = gen_fp_oper "gfp"
   val Tarski    = def_gfp_Tarski
   val induct    = def_Collect_coinduct
diff -r 61fd5c1d733f -r 8b65444edbb0 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed May 27 12:19:35 1998 +0200
+++ b/src/HOL/Tools/record_package.ML	Wed May 27 12:21:39 1998 +0200
@@ -621,7 +621,7 @@
 
 fun gen_add_record prep_typ prep_raw_parent (params, bname) raw_parent raw_fields thy =
   let
-    val _ = Theory.require thy "Record" "record definitions";
+    val _ = Theory.requires thy "Record" "record definitions";
     val sign = Theory.sign_of thy;
     val _ = writeln ("Defining record " ^ quote bname ^ " ...");
 
diff -r 61fd5c1d733f -r 8b65444edbb0 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Wed May 27 12:19:35 1998 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Wed May 27 12:21:39 1998 +0200
@@ -43,7 +43,7 @@
 
 fun gen_add_typedef prep_term name (t, vs, mx) raw_set axms thms usr_tac thy =
   let
-    val _ = Theory.require thy "Set" "typedefs";
+    val _ = Theory.requires thy "Set" "typedefs";
     val sign = sign_of thy;
     val full_name = Sign.full_name sign;
 
diff -r 61fd5c1d733f -r 8b65444edbb0 src/HOL/datatype.ML
--- a/src/HOL/datatype.ML	Wed May 27 12:19:35 1998 +0200
+++ b/src/HOL/datatype.ML	Wed May 27 12:21:39 1998 +0200
@@ -209,7 +209,7 @@
 in
   fun add_datatype (typevars, tname, cons_list') thy = 
     let
-      val dummy = Theory.require thy "Arith" "datatype definitions";
+      val dummy = Theory.requires thy "Arith" "datatype definitions";
       
       fun typid(dtRek(_,id)) = id
         | typid(dtVar s) = implode (tl (explode s))
diff -r 61fd5c1d733f -r 8b65444edbb0 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Wed May 27 12:19:35 1998 +0200
+++ b/src/Pure/theory.ML	Wed May 27 12:21:39 1998 +0200
@@ -84,7 +84,7 @@
   val put_data: string * object -> theory -> theory
   val prep_ext: theory -> theory
   val prep_ext_merge: theory list -> theory
-  val require: theory -> string -> string -> unit
+  val requires: theory -> string -> string -> unit
   val pre_pure: theory
 end;
 
@@ -125,7 +125,7 @@
 val eq_thy = Sign.eq_sg o pairself sign_of;
 
 (*check for some named theory*)
-fun require thy name what =
+fun requires thy name what =
   if exists (equal name) (Sign.stamp_names_of (sign_of thy)) then ()
   else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
 
diff -r 61fd5c1d733f -r 8b65444edbb0 src/ZF/add_ind_def.ML
--- a/src/ZF/add_ind_def.ML	Wed May 27 12:19:35 1998 +0200
+++ b/src/ZF/add_ind_def.ML	Wed May 27 12:21:39 1998 +0200
@@ -72,7 +72,7 @@
 fun add_fp_def_i (rec_tms, dom_sum, intr_tms) thy = 
   let
     val dummy = (*has essential ancestors?*)
-	Theory.require thy "Inductive" "(co)inductive definitions" 
+	Theory.requires thy "Inductive" "(co)inductive definitions" 
 
     val sign = sign_of thy;
 
@@ -178,7 +178,7 @@
 fun add_constructs_def (rec_base_names, con_ty_lists) thy = 
   let
     val dummy = (*has essential ancestors?*)
-      Theory.require thy "Datatype" "(co)datatype definitions";
+      Theory.requires thy "Datatype" "(co)datatype definitions";
 
     val sign = sign_of thy;
     val full_name = Sign.full_name sign;