# HG changeset patch
# User wenzelm
# Date 1261060738 -3600
# Node ID 9274a44358c4341ced87ea9a884e9be0ab21dd48
# Parent  e438a5875c16f888e19c38f39037e2192502b057
tuned;

diff -r e438a5875c16 -r 9274a44358c4 src/Pure/Thy/completion.scala
--- a/src/Pure/Thy/completion.scala	Thu Dec 17 15:09:07 2009 +0100
+++ b/src/Pure/Thy/completion.scala	Thu Dec 17 15:38:58 2009 +0100
@@ -32,7 +32,7 @@
 
     override def toString: String =
     {
-      val buf = new StringBuffer(length)
+      val buf = new StringBuilder(length)
       for (i <- 0 until length)
         buf.append(charAt(i))
       buf.toString