# HG changeset patch
# User wenzelm
# Date 1206635756 -3600
# Node ID e38f7e1c07ce4ad2a5d31b5e2a9c4377aedf05bc
# Parent  090ced25100933a10596774539f53435331c4f73
tuned comments;

diff -r 090ced251009 -r e38f7e1c07ce src/Pure/library.ML
--- 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