improved terminator msg;
authorwenzelm
Sun, 04 Jun 2000 00:00:17 +0200
changeset 9033 f12d8ea8618b
parent 9032 ad0b9f048bbf
child 9034 ea4dc7603f0b
improved terminator msg;
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