# HG changeset patch
# User berghofe
# Date 999266965 -7200
# Node ID a12def3d1847f5c8dfaef28836308b135ae34f30
# Parent  2f6fe5b0152186a44705167d7bdb8d870838821a
Added function unique_strings.

diff -r 2f6fe5b01521 -r a12def3d1847 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Aug 31 16:08:45 2001 +0200
+++ b/src/Pure/library.ML	Fri Aug 31 16:09:25 2001 +0200
@@ -232,6 +232,7 @@
   val sort: ('a * 'a -> order) -> 'a list -> 'a list
   val sort_strings: string list -> string list
   val sort_wrt: ('a -> string) -> 'a list -> 'a list
+  val unique_strings: string list -> string list
 
   (*I/O and diagnostics*)
   val cd: string -> unit
@@ -1127,6 +1128,11 @@
 val sort_strings = sort string_ord;
 fun sort_wrt sel xs = sort (string_ord o pairself sel) xs;
 
+fun unique_strings ([]: string list) = []
+  | unique_strings [x] = [x]
+  | unique_strings (x :: y :: ys) =
+      if x = y then unique_strings (y :: ys)
+      else x :: unique_strings (y :: ys);
 
 
 (** input / output and diagnostics **)