# HG changeset patch
# User wenzelm
# Date 1004306319 -3600
# Node ID a394d3e9c8bbd8e415f1e7cd21df8e2618f52e28
# Parent  2e7c54b867638ebc7805c3f1cea87ed5c59c336f
fixed string_of_mixfix;

diff -r 2e7c54b86763 -r a394d3e9c8bb src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Sun Oct 28 21:14:56 2001 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Sun Oct 28 22:58:39 2001 +0100
@@ -83,7 +83,9 @@
   | string_of_mixfix (InfixrName (sy, p)) = parens (spaces ["infixl", quote sy, string_of_int p])
   | string_of_mixfix (Infix p) = parens (spaces ["infix", string_of_int p])
   | 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 (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]);
 
 
 (* type / const names *)