src/Pure/library.ML

   val prefix_lines: string -> string -> string
   val split_lines: string -> string list
   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
   val mem_int: int * int list -> bool
   val mem_string: string * string list -> bool

     if prfx_len >= 0 andalso implode (drop (prfx_len, cs)) = sfx then
       implode (take (prfx_len, cs))
     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 **)
 
 (*membership in a list*)