fixed string_of_mixfix;
authorwenzelm
Sun, 28 Oct 2001 22:58:39 +0100
changeset 11978 a394d3e9c8bb
parent 11977 2e7c54b86763
child 11979 0a3dace545c5
fixed string_of_mixfix;
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 *)