# HG changeset patch
# User wenzelm
# Date 927279615 -7200
# Node ID e33ae2af0d361788f732c6b224e9104be3438a8a
# Parent  4f859545bd92240dc2158f3956dfdd4ac5176cc0
tuned;

diff -r 4f859545bd92 -r e33ae2af0d36 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri May 21 11:39:47 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri May 21 11:40:15 1999 +0200
@@ -21,8 +21,6 @@
   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 ->
@@ -53,9 +51,6 @@
 
 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 *)
 
@@ -297,8 +292,9 @@
 
 
 (*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;