added replicate_string;

--- a/src/Pure/library.ML	Sun Jan 21 19:50:43 2001 +0100
+++ b/src/Pure/library.ML	Sun Jan 21 19:52:32 2001 +0100
@@ -157,6 +157,7 @@
   val untabify: string list -> string list
   val suffix: string -> string -> string
   val unsuffix: string -> string -> string
+  val replicate_string: int -> string -> string
 
   (*lists as sets*)
   val mem: ''a * ''a list -> bool
@@ -771,6 +772,12 @@
     else raise LIST "unsuffix"
   end;
 
+fun replicate_string 0 _ = ""
+  | replicate_string 1 a = a
+  | replicate_string k a =
+      if k mod 2 = 0 then replicate_string (k div 2) (a ^ a)
+      else replicate_string (k div 2) (a ^ a) ^ a;
+
 
 
 (** lists as sets **)