author | wenzelm |
Sun, 04 Jun 2000 00:00:17 +0200 | |
changeset 9033 | f12d8ea8618b |
parent 9032 | ad0b9f048bbf |
child 9034 | ea4dc7603f0b |
--- 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