--- a/src/Pure/library.ML Thu Mar 27 17:21:41 2008 +0100
+++ b/src/Pure/library.ML Thu Mar 27 17:35:56 2008 +0100
@@ -793,7 +793,8 @@
(** lists as sets -- see also Pure/General/ord_list.ML **)
-(*canonical member, insert, remove*)
+(* canonical operations *)
+
fun member eq list x =
let
fun memb [] = false
@@ -809,12 +810,13 @@
fun merge _ ([], ys) = ys
| merge eq (xs, ys) = fold_rev (insert eq) ys xs;
-(*old-style infixes*)
+
+(* old-style infixes *)
+
fun x mem xs = member (op =) xs x;
fun (x: int) mem_int xs = member (op =) xs x;
fun (x: string) mem_string xs = member (op =) xs x;
-
(*union of sets represented as lists: no repetitions*)
fun xs union [] = xs
| [] union ys = ys