# HG changeset patch
# User wenzelm
# Date 980103152 -3600
# Node ID ddb9b820d8a5d796f04c8273281810576d87e844
# Parent  aa788fcb75a5812d958428661f482af3a04e38b2
added replicate_string;

diff -r aa788fcb75a5 -r ddb9b820d8a5 src/Pure/library.ML
--- 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 **)