Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Syntax/mixfix.ML
changeset 18341 d99396e96632
parent 18024 853e8219732a
child 18565 818a24371de9 
--- 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 *)
isabelle