src/Pure/Isar/outer_syntax.ML

     (bool -> local_theory -> Proof.state) parser -> unit
   val local_theory_to_proof: command_spec -> string ->
     (local_theory -> Proof.state) parser -> unit
   val help_outer_syntax: string list -> unit
   val print_outer_syntax: unit -> unit
-  val scan: Position.T -> string -> Token.T list
-  val parse: Position.T -> string -> Toplevel.transition list
-  val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
+  val scan: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
+  val parse: (Scan.lexicon * Scan.lexicon) * outer_syntax ->
+    Position.T -> string -> Toplevel.transition list
   val parse_spans: Token.T list -> Command_Span.span list
   type isar
   val isar: TextIO.instream -> bool -> isar
   val side_comments: Token.T list -> Token.T list
   val command_reports: outer_syntax -> Token.T -> Position.report_text list

   end;
 
 
 (* off-line scanning/parsing *)
 
-fun scan pos str =
-  Source.of_string str
-  |> Symbol.source
-  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
-  |> Source.exhaust;
-
-fun parse pos str =
-  Source.of_string str
-  |> Symbol.source
-  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
-  |> toplevel_source false NONE lookup_commands_dynamic
-  |> Source.exhaust;
-
-fun parse_tokens lexs pos =
+fun scan lexs pos =
   Source.of_string #>
   Symbol.source #>
   Token.source {do_recover = SOME false} (K lexs) pos #>
   Source.exhaust;
+
+fun parse (lexs, syntax) pos str =
+  Source.of_string str
+  |> Symbol.source
+  |> Token.source {do_recover = SOME false} (K lexs) pos
+  |> toplevel_source false NONE (K (lookup_commands syntax))
+  |> Source.exhaust;
 
 
 (* parse spans *)
 
 local