| changeset 14559 | 7612d19d5638 |
| parent 14557 | 31ae4a47267c |
| child 14561 | c53396af770e |
--- a/src/Pure/General/symbol.ML Wed Apr 14 09:53:25 2004 +0200 +++ b/src/Pure/General/symbol.ML Wed Apr 14 10:08:28 2004 +0200 @@ -208,8 +208,8 @@ (* scan *) val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode); -val scan_ctrlid = Scan.one is_letter ^^ (Scan.any is_ctrl_letter >> implode); -val scan_rawctrlid = $$ "r" ^^ $$ "a" ^^ $$ "w" ^^ scan_ctrlid; +val scan_rawctrlid = + $$ "r" ^^ $$ "a" ^^ $$ "w" ^^ (Scan.any is_ctrl_letter >> implode); val scan = $$ "\\" ^^ $$ "<" ^^