| changeset 40523 | 1050315f6ee2 |
| parent 38149 | 3c380380beac |
| child 40530 | f814863f3918 |
--- a/src/Pure/Thy/thy_header.ML Sat Nov 13 16:46:00 2010 +0100 +++ b/src/Pure/Thy/thy_header.ML Sat Nov 13 19:21:53 2010 +0100 @@ -57,7 +57,7 @@ let val res = str |> Source.of_string_limited 8000 - |> Symbol.source {do_recover = false} + |> Symbol.source |> Token.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos |> Token.source_proper |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE