src/Pure/Isar/outer_syntax.ML

       (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
   in
     src
     |> Token.source_proper
     |> Source.source Token.stopper
-      (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source >> K NONE || Parse.not_eof >> SOME))
+      (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.document_source >> K NONE || Parse.not_eof >> SOME))
         (Option.map recover do_recover)
     |> Source.map_filter I
     |> Source.source Token.stopper
         (Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
         (Option.map recover do_recover)