1.1 --- a/src/Pure/Thy/thy_output.ML	Sat Jul 23 16:12:12 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Jul 23 16:37:17 2011 +0200
     1.3 @@ -355,7 +355,7 @@
     1.4    Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore
     1.5      >> pair (d + 1)) ||
     1.6    Scan.depend (fn d => Scan.one Token.is_end_ignore --|
     1.7 -    (if d = 0 then Scan.fail_with (K "Bad nesting of meta-comments") else opt_newline)
     1.8 +    (if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
     1.9      >> pair (d - 1));
    1.10  
    1.11  val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end);