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