diff -r a5e7574d8214 -r 3ff725ac13a4 src/Pure/Thy/markup_node.scala
--- a/src/Pure/Thy/markup_node.scala	Mon Mar 29 01:07:01 2010 -0700
+++ b/src/Pure/Thy/markup_node.scala	Mon Mar 29 22:43:56 2010 +0200
@@ -70,7 +70,7 @@
           markup <- markups
         } yield markup
       if (next_x < node.stop)
-        filled_gaps + new Markup_Node(next_x, node.stop, node.info)
+        filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info))
       else filled_gaps
     }
   }