src/Pure/Isar/outer_syntax.ML

 signature OUTER_SYNTAX =
 sig
   include BASIC_OUTER_SYNTAX
   type token
   type parser
-  val parser: bool -> string -> string ->
-    (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
   val command: string -> string ->
     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
   val improper_command: string -> string ->
     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
   val print_outer_syntax: unit -> unit

 
 datatype parser =
   Parser of string * string * bool * parser_fn;
 
 fun parser int_only name comment parse = Parser (name, comment, int_only, parse);
-
-val command_parser = parser false;
-val improper_command_parser = parser true;
 
 
 (* parse command *)
 
 local open OuterParse in

   writeln ("This is Isabelle's underlying ML system (" ^ ml_system ^ ");\n\
     \invoke 'loop();' to enter the Isar loop.");
 
 
 (*final declarations of this structure!*)
-val command = command_parser;
-val improper_command = improper_command_parser;
+val command = parser false;
+val improper_command = parser true;
+
 
 end;
 
 (*setup theory syntax dependent operations*)
 ThyLoad.deps_thy_fn := OuterSyntax.deps_thy;