diff -r 63a16e98cc14 -r 64e571275b36 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Sat Nov 01 15:35:40 2014 +0100
+++ b/src/Pure/Isar/token.ML	Sat Nov 01 18:46:48 2014 +0100
@@ -79,9 +79,9 @@
   val pretty_src: Proof.context -> src -> Pretty.T
   val ident_or_symbolic: string -> bool
   val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
-  val source': {do_recover: bool option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
+  val source': {do_recover: bool} -> (unit -> Scan.lexicon * Scan.lexicon) ->
     (Symbol_Pos.T, 'a) Source.source -> (T, (Symbol_Pos.T, 'a) Source.source) Source.source
-  val source: {do_recover: bool option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
+  val source: {do_recover: bool} -> (unit -> Scan.lexicon * Scan.lexicon) ->
     Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
       (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
   type 'a parser = T list -> 'a * T list
@@ -562,7 +562,7 @@
 
 fun source' {do_recover} get_lex =
   Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
-    (Option.map (rpair recover) do_recover);
+    (if do_recover then SOME recover else NONE);
 
 fun source do_recover get_lex pos src =
   Symbol_Pos.source pos src
@@ -582,7 +582,7 @@
 
 fun read lex scan (syms, pos) =
   Source.of_list syms
-  |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
+  |> source' {do_recover = false} (K (lex, Scan.empty_lexicon))
   |> source_proper
   |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
   |> Source.exhaust;