src/HOL/Tools/record_package.ML

 (*we do all preparations and error checks here, deferring the real
   work to record_definition*)
 
 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 ^ " ...");
 
 
     (* parents *)