--- a/src/Pure/General/ord_list.ML Thu Oct 16 22:44:34 2008 +0200
+++ b/src/Pure/General/ord_list.ML Thu Oct 16 22:44:35 2008 +0200
@@ -9,6 +9,7 @@
signature ORD_LIST =
sig
type 'a T = 'a list
+ val make: ('a * 'a -> order) -> 'a list -> 'a T
val member: ('b * 'a -> order) -> 'a T -> 'b -> bool
val insert: ('a * 'a -> order) -> 'a -> 'a T -> 'a T
val remove: ('b * 'a -> order) -> 'b -> 'a T -> 'a T
@@ -22,6 +23,7 @@
struct
type 'a T = 'a list;
+fun make ord = sort_distinct ord;
(* single elements *)