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