src/Pure/Isar/outer_syntax.ML

     (local_theory -> local_theory) parser -> unit
   val local_theory_to_proof': command_spec -> string ->
     (bool -> local_theory -> Proof.state) parser -> unit
   val local_theory_to_proof: command_spec -> string ->
     (local_theory -> Proof.state) parser -> unit
-  val scan: Keyword.keywords -> Position.T -> string -> Token.T list
   val parse: theory -> Position.T -> string -> Toplevel.transition list
   val parse_tokens: theory -> Token.T list -> Toplevel.transition list
   val parse_spans: Token.T list -> Command_Span.span list
   val side_comments: Token.T list -> Token.T list
   val command_reports: theory -> Token.T -> Position.report_text list

 val local_theory_to_proof = local_theory_command Toplevel.local_theory_to_proof;
 
 
 
 (** toplevel parsing **)
-
-(* scan tokens *)
-
-fun scan keywords pos =
-  Source.of_string #>
-  Symbol.source #>
-  Token.source keywords pos #>
-  Source.exhaust;
-
 
 (* parse commands *)
 
 local