src/HOL/Tools/typedef_package.ML
changeset 7152 44d46a112127
parent 6935 a3f3f4128cab
child 7481 d44c77be268c
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Mon Aug 02 17:58:00 1999 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Mon Aug 02 17:58:23 1999 +0200
     1.3 @@ -209,7 +209,7 @@
     1.4  
     1.5  val typedeclP =
     1.6    OuterSyntax.command "typedecl" "HOL type declaration" K.thy_decl
     1.7 -    (P.type_args -- P.name -- P.opt_mixfix --| P.marg_comment >> (fn ((vs, t), mx) =>
     1.8 +    (P.type_args -- P.name -- P.opt_infix --| P.marg_comment >> (fn ((vs, t), mx) =>
     1.9        Toplevel.theory (add_typedecls [(t, vs, mx)])));
    1.10  
    1.11