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;