author | wenzelm |
Fri, 15 Aug 2008 21:57:22 +0200 | |
changeset 27903 | af1b39debf30 |
parent 27902 | 4a419fd52f44 |
child 27904 | 343696007eca |
--- a/src/Pure/General/symbol.ML Fri Aug 15 21:56:07 2008 +0200 +++ b/src/Pure/General/symbol.ML Fri Aug 15 21:57:22 2008 +0200 @@ -446,7 +446,7 @@ Scan.this_string "{*" || Scan.this_string "*}"; val recover = - Scan.this (explode "\\<") @@@ + (Scan.this (explode "\\\\<") || Scan.this (explode "\\<")) @@@ Scan.repeat (Scan.unless scan_resync (Scan.one not_eof)) >> (fn ss => malformed :: ss @ [end_malformed]);