# HG changeset patch
# User wenzelm
# Date 1133560491 -3600
# Node ID d99396e9663299c86074c564789c3056b54225d5
# Parent  3fdff270aa04ee540dec430c8700cb503d814846
mixfix_args: 1 for binders;
string_of_mixfix: proper output of binders;

diff -r 3fdff270aa04 -r d99396e96632 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Dec 02 22:54:50 2005 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Fri Dec 02 22:54:51 2005 +0100
@@ -85,7 +85,7 @@
   | string_of_mixfix (Infixl p) = parens (spaces ["infixl", string_of_int p])
   | string_of_mixfix (Infixr p) = parens (spaces ["infixr", string_of_int p])
   | string_of_mixfix (Binder (sy, p1, p2)) =
-      parens (spaces ["binder", brackets (string_of_int p1), string_of_int p2]);
+      parens (spaces ["binder", quote sy, brackets (string_of_int p1), string_of_int p2]);
 
 
 (* syntax specifications *)
@@ -126,7 +126,10 @@
   | mixfix_args (InfixName (sy, _)) = 2 + SynExt.mfix_args sy
   | mixfix_args (InfixlName (sy, _)) = 2 + SynExt.mfix_args sy
   | mixfix_args (InfixrName (sy, _)) = 2 + SynExt.mfix_args sy
-  | mixfix_args (*old infix or binder*) _ = 2;
+  | mixfix_args (Infix _) = 2
+  | mixfix_args (Infixl _) = 2
+  | mixfix_args (Infixr _) = 2
+  | mixfix_args (Binder _) = 1;
 
 
 (* syn_ext_types *)