| changeset 4970 | 8b65444edbb0 |
| parent 4932 | c90411dde8e8 |
| child 5104 | 230cca8452c7 |
--- 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;