# HG changeset patch
# User wenzelm
# Date 1364040268 -3600
# Node ID 38a796ac4ab7cd16bc3d1db6d04d8dc093f9d80b
# Parent  0a0c9a45d294459c6c60fb3f4dfd7c71a8bf753e
tuned;

diff -r 0a0c9a45d294 -r 38a796ac4ab7 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sat Mar 23 07:30:53 2013 +0100
+++ b/src/Pure/General/pretty.ML	Sat Mar 23 13:04:28 2013 +0100
@@ -79,12 +79,13 @@
 (** spaces **)
 
 local
-  val small_spaces = Vector.tabulate (65, fn i => Library.replicate_string i Symbol.space);
+  val small_spaces = Vector.tabulate (65, fn i => replicate_string i Symbol.space);
 in
   fun spaces k =
     if k < 64 then Vector.sub (small_spaces, k)
-    else Library.replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^
-      Vector.sub (small_spaces, k mod 64);
+    else
+      replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^
+        Vector.sub (small_spaces, k mod 64);
 end;