src/Pure/Isar/outer_syntax.ML
changeset 9033 f12d8ea8618b
parent 8999 ad8260dc6e4a
child 9036 d9e09ef531dd
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Jun 03 23:59:37 2000 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sun Jun 04 00:00:17 2000 +0200
     1.3 @@ -126,7 +126,7 @@
     1.4    | None => sys_error ("no parser for outer syntax command " ^ quote name));
     1.5  
     1.6  fun terminator false = Scan.succeed ()
     1.7 -  | terminator true = P.group "terminator" (Scan.option P.sync -- P.$$$ ";" >> K ());
     1.8 +  | terminator true = P.group "end of input" (Scan.option P.sync -- P.$$$ ";" >> K ());
     1.9  
    1.10  in
    1.11