src/Pure/ML/ml_lex.ML

     val scan = if SML then scan_ml >> Antiquote.Text else scan_antiq;
     fun check (Antiquote.Text tok) = (check_content_of tok; if SML then () else warn tok)
       | check _ = ();
     val input =
       Source.of_list syms
-      |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan))
-        (SOME (fn msg => recover msg >> map Antiquote.Text))
+      |> Source.source Symbol_Pos.stopper
+        (Scan.recover (Scan.bulk (!!! "bad input" scan))
+          (fn msg => recover msg >> map Antiquote.Text))
       |> Source.exhaust
       |> tap (Position.reports_text o Antiquote.antiquote_reports (single o report_of_token SML))
       |> tap (List.app check);
   in input @ termination end;
 
 in
 
 fun source src =
   Symbol_Pos.source (Position.line 1) src
-  |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME recover);
+  |> Source.source Symbol_Pos.stopper (Scan.recover (Scan.bulk (!!! "bad input" scan_ml)) recover);
 
 val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust;
 
 val read = gen_read false;