src/Pure/theory.ML

     (object * object -> object) * (Sign.sg -> object -> unit))) list -> theory -> theory
   val get_data: theory -> string -> object
   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;
 
 
 structure Theory: THEORY =

 (*compare theories*)
 val subthy = Sign.subsig o pairself sign_of;
 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);
 
 (*partial Pure theory*)
 val pre_pure = make_thy Sign.pre_pure Symtab.empty Symtab.empty [] [];