src/HOL/Tools/typedef_package.ML
changeset 4970 8b65444edbb0
parent 4932 c90411dde8e8
child 5104 230cca8452c7
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Wed May 27 12:19:35 1998 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Wed May 27 12:21:39 1998 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4  
     1.5  fun gen_add_typedef prep_term name (t, vs, mx) raw_set axms thms usr_tac thy =
     1.6    let
     1.7 -    val _ = Theory.require thy "Set" "typedefs";
     1.8 +    val _ = Theory.requires thy "Set" "typedefs";
     1.9      val sign = sign_of thy;
    1.10      val full_name = Sign.full_name sign;
    1.11