diff -r f8715e7c1be6 -r b979c781c2db src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Tools/Code/code_printer.ML	Fri Oct 31 22:02:49 2014 +0100
@@ -373,7 +373,7 @@
 
 fun read_mixfix s =
   let
-    val sym_any = Scan.one Symbol.is_regular;
+    val sym_any = Scan.one Symbol.not_eof;
     val parse = Scan.optional ($$ "!" >> K NOBR) BR -- Scan.repeat (
          ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
       || ($$ "_" >> K (Arg BR))