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;