src/Pure/Isar/outer_syntax.ML
changeset 40523 1050315f6ee2
parent 38422 f96394dba335
child 41484 51310e1ccd6f
--- a/src/Pure/Isar/outer_syntax.ML	Sat Nov 13 16:46:00 2010 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Nov 13 19:21:53 2010 +0100
@@ -187,13 +187,13 @@
 
 fun scan pos str =
   Source.of_string str
-  |> Symbol.source {do_recover = false}
+  |> Symbol.source
   |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
   |> Source.exhaust;
 
 fun parse pos str =
   Source.of_string str
-  |> Symbol.source {do_recover = false}
+  |> Symbol.source
   |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
   |> toplevel_source false NONE get_command
   |> Source.exhaust;
@@ -224,7 +224,7 @@
 
 fun isar in_stream term : isar =
   Source.tty in_stream
-  |> Symbol.source {do_recover = true}
+  |> Symbol.source
   |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
   |> toplevel_source term (SOME true) get_command;