# HG changeset patch
# User wenzelm
# Date 960069617 -7200
# Node ID f12d8ea8618bcc4464bb10a37c81c2e23230bf96
# Parent  ad0b9f048bbf8bceca385fd446264db34634368f
improved terminator msg;

diff -r ad0b9f048bbf -r f12d8ea8618b src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Sat Jun 03 23:59:37 2000 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Sun Jun 04 00:00:17 2000 +0200
@@ -126,7 +126,7 @@
   | None => sys_error ("no parser for outer syntax command " ^ quote name));
 
 fun terminator false = Scan.succeed ()
-  | terminator true = P.group "terminator" (Scan.option P.sync -- P.$$$ ";" >> K ());
+  | terminator true = P.group "end of input" (Scan.option P.sync -- P.$$$ ";" >> K ());
 
 in