src/Pure/Isar/isar_syn.ML
changeset 35351 7425aece4ee3
parent 35315 fbdc860d87a3
child 35413 4c7cba1f7ce9
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Feb 24 07:06:39 2010 -0800
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Feb 24 20:37:01 2010 +0100
     1.3 @@ -104,13 +104,13 @@
     1.4  
     1.5  val _ =
     1.6    OuterSyntax.command "typedecl" "type declaration" K.thy_decl
     1.7 -    (P.type_args -- P.binding -- P.opt_infix >> (fn ((args, a), mx) =>
     1.8 +    (P.type_args -- P.binding -- P.opt_mixfix >> (fn ((args, a), mx) =>
     1.9        Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd)));
    1.10  
    1.11  val _ =
    1.12    OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
    1.13      (Scan.repeat1
    1.14 -      (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')))
    1.15 +      (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix')))
    1.16        >> (Toplevel.theory o Sign.add_tyabbrs o
    1.17          map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
    1.18