src/Pure/Thy/thy_header.ML
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