diff -r f6a2e5ce2ce5 -r 5f5649ac8235 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Sun Aug 21 20:25:49 2011 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Sun Aug 21 20:42:26 2011 +0200 @@ -62,7 +62,9 @@ local fun terminate false = Scan.succeed () - | terminate true = Parse.group "end of input" (Scan.option Parse.sync -- Parse.semicolon >> K ()); + | terminate true = + Parse.group (fn () => "end of input") + (Scan.option Parse.sync -- Parse.semicolon >> K ()); fun body cmd (name, _) = (case cmd name of