diff -r a974f66062c8 -r afddf4e26fac src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Fri Oct 12 22:53:20 2012 +0200
+++ b/src/Pure/General/pretty.scala	Fri Oct 12 23:38:48 2012 +0200
@@ -60,7 +60,7 @@
   val FBreak = XML.Text("\n")
 
   val Separator = List(XML.elem(Isabelle_Markup.SEPARATOR, List(XML.Text(space))), FBreak)
-  def separate(ts: List[XML.Tree]): XML.Body = ts.map(t => t :: Separator).flatten
+  def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
 
 
   /* formatted output */