src/ZF/add_ind_def.ML

 
 (*internal version*)
 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;
 
     (*recT and rec_params should agree for all mutually recursive components*)
     val rec_hds = map head_of rec_tms;

 (*Expects the recursive sets to have been defined already.
   con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
 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;
 
     val dummy = writeln"  Defining the constructor functions...";