# HG changeset patch
# User wenzelm
# Date 1224189875 -7200
# Node ID f65736dfc40d59eb464b3682caddbde8e9c16dcb
# Parent  d51a14105e5367820cae58d90bdedb87b32796ab
added make;

diff -r d51a14105e53 -r f65736dfc40d src/Pure/General/ord_list.ML
--- 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 *)