changeset 58863 | 64e571275b36 |
parent 58861 | 5ff61774df11 |
child 58864 | 505a8150368a |
--- a/src/Pure/Thy/thy_header.ML Sat Nov 01 15:35:40 2014 +0100 +++ b/src/Pure/Thy/thy_header.ML Sat Nov 01 18:46:48 2014 +0100 @@ -127,7 +127,7 @@ str |> Source.of_string_limited 8000 |> Symbol.source - |> Token.source {do_recover = NONE} (K header_lexicons) pos; + |> Token.source {do_recover = false} (K header_lexicons) pos; fun read_source pos source = let val res =