src/Pure/ML/ml_lex.ML

 
 fun source src =
   Symbol_Pos.source (Position.line 1) src
   |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
 
-val tokenize =
-  Source.of_string #>
-  Symbol.source {do_recover = true} #>
-  source #>
-  Source.exhaust;
+val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust;
 
 fun read pos txt =
   let
     val _ = Position.report pos Markup.ML_source;
     val syms = Symbol_Pos.explode (txt, pos);