# HG changeset patch
# User berghofe
# Date 1125078443 -7200
# Node ID bc97adfeeaa740ad427e1172793b6f58dc4f36a4
# Parent  ce2a1aeb42aaa031159e29d3dfe17dc123dd09d3
Fixed bug.

diff -r ce2a1aeb42aa -r bc97adfeeaa7 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Fri Aug 26 19:36:07 2005 +0200
+++ b/src/Pure/Isar/isar_output.ML	Fri Aug 26 19:47:23 2005 +0200
@@ -247,8 +247,7 @@
     (tag_stack, active_tag, newline, buffer, present_cont) =
   let
     val present = fold (fn (raw, tok, d) =>
-      if d > 0 then I
-      else Buffer.add raw #> Buffer.add (output_token lex state' tok));
+      Buffer.add raw o (if d > 0 then I else Buffer.add (output_token lex state' tok)));
 
     val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;