src/Pure/Syntax/mixfix.ML
changeset 18341 d99396e96632
parent 18024 853e8219732a
child 18565 818a24371de9
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Dec 02 22:54:50 2005 +0100
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Dec 02 22:54:51 2005 +0100
     1.3 @@ -85,7 +85,7 @@
     1.4    | string_of_mixfix (Infixl p) = parens (spaces ["infixl", string_of_int p])
     1.5    | string_of_mixfix (Infixr p) = parens (spaces ["infixr", string_of_int p])
     1.6    | string_of_mixfix (Binder (sy, p1, p2)) =
     1.7 -      parens (spaces ["binder", brackets (string_of_int p1), string_of_int p2]);
     1.8 +      parens (spaces ["binder", quote sy, brackets (string_of_int p1), string_of_int p2]);
     1.9  
    1.10  
    1.11  (* syntax specifications *)
    1.12 @@ -126,7 +126,10 @@
    1.13    | mixfix_args (InfixName (sy, _)) = 2 + SynExt.mfix_args sy
    1.14    | mixfix_args (InfixlName (sy, _)) = 2 + SynExt.mfix_args sy
    1.15    | mixfix_args (InfixrName (sy, _)) = 2 + SynExt.mfix_args sy
    1.16 -  | mixfix_args (*old infix or binder*) _ = 2;
    1.17 +  | mixfix_args (Infix _) = 2
    1.18 +  | mixfix_args (Infixl _) = 2
    1.19 +  | mixfix_args (Infixr _) = 2
    1.20 +  | mixfix_args (Binder _) = 1;
    1.21  
    1.22  
    1.23  (* syn_ext_types *)