# HG changeset patch
# User wenzelm
# Date 1119298446 -7200
# Node ID fbfd15412f055fb104ed6ebdf55c67bcd96a7e85
# Parent  7310d0a365995adde4fa9c2291d48bf3dd51abd1
added member, option_ord;

diff -r 7310d0a36599 -r fbfd15412f05 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Jun 20 22:14:05 2005 +0200
+++ b/src/Pure/library.ML	Mon Jun 20 22:14:06 2005 +0200
@@ -166,7 +166,7 @@
   val replicate_string: int -> string -> string
   val translate_string: (string -> string) -> string -> string
 
-  (*lists as sets*)
+  (*lists as sets -- see also Pure/General/ord_list.ML*)
   val mem: ''a * ''a list -> bool
   val mem_int: int * int list -> bool
   val mem_string: string * string list -> bool
@@ -175,6 +175,7 @@
   val ins_int: int * int list -> int list
   val ins_string: string * string list -> string list
   val gen_ins: ('a * 'a -> bool) -> 'a * 'a list -> 'a list
+  val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
   val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
   val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
   val union: ''a list * ''a list -> ''a list
@@ -231,6 +232,7 @@
   val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
   val int_ord: int * int -> order
   val string_ord: string * string -> order
+  val option_ord: ('a * 'b -> order) -> 'a option * 'b option -> order
   val prod_ord: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order
   val dict_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
   val list_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
@@ -817,7 +819,7 @@
 
 
 
-(** lists as sets **)
+(** lists as sets -- see also Pure/General/ord_list.ML **)
 
 (*membership in a list*)
 fun x mem [] = false
@@ -835,7 +837,8 @@
 fun gen_mem eq (x, []) = false
   | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys);
 
-(*insert and remove*)
+(*member, insert, and remove -- with canonical argument order*)
+fun member eq xs x = gen_mem eq (x, xs);
 fun insert eq x xs = if gen_mem eq (x, xs) then xs else x :: xs;
 fun remove eq x xs = if gen_mem eq (x, xs) then filter_out (fn y => eq (x, y)) xs else xs;
 
@@ -1085,6 +1088,11 @@
 val int_ord = Int.compare;
 val string_ord = String.compare;
 
+fun option_ord ord (SOME x, SOME y) = ord (x, y)
+  | option_ord _ (NONE, NONE) = EQUAL
+  | option_ord _ (NONE, SOME _) = LESS
+  | option_ord _ (SOME _, NONE) = GREATER;
+
 (*lexicographic product*)
 fun prod_ord a_ord b_ord ((x, y), (x', y')) =
   (case a_ord (x, x') of EQUAL => b_ord (y, y') | ord => ord);