author | wenzelm |
Thu, 18 Mar 2010 22:59:44 +0100 | |
changeset 35835 | 51c6ac100bd9 |
parent 35834 | 0c71e0d72d7a |
child 35836 | 9380fab5f4f7 |
--- a/src/Pure/Isar/isar_syn.ML Thu Mar 18 22:56:32 2010 +0100 +++ b/src/Pure/Isar/isar_syn.ML Thu Mar 18 22:59:44 2010 +0100 @@ -105,7 +105,7 @@ val _ = OuterSyntax.local_theory "typedecl" "type declaration" K.thy_decl (P.type_args -- P.binding -- P.opt_mixfix - >> (fn ((args, a), mx) => Typedecl.typedecl (a, args, mx) #> snd)); + >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd)); val _ = OuterSyntax.command "types" "declare type abbreviations" K.thy_decl