tuned comments;
authorwenzelm
Thu Mar 27 17:35:56 2008 +0100 (2008-03-27)
changeset 26439e38f7e1c07ce
parent 26438 090ced251009
child 26440 feeb83f9657f
tuned comments;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Mar 27 17:21:41 2008 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Mar 27 17:35:56 2008 +0100
     1.3 @@ -793,7 +793,8 @@
     1.4  
     1.5  (** lists as sets -- see also Pure/General/ord_list.ML **)
     1.6  
     1.7 -(*canonical member, insert, remove*)
     1.8 +(* canonical operations *)
     1.9 +
    1.10  fun member eq list x =
    1.11    let
    1.12      fun memb [] = false
    1.13 @@ -809,12 +810,13 @@
    1.14  fun merge _ ([], ys) = ys
    1.15    | merge eq (xs, ys) = fold_rev (insert eq) ys xs;
    1.16  
    1.17 -(*old-style infixes*)
    1.18 +
    1.19 +(* old-style infixes *)
    1.20 +
    1.21  fun x mem xs = member (op =) xs x;
    1.22  fun (x: int) mem_int xs = member (op =) xs x;
    1.23  fun (x: string) mem_string xs = member (op =) xs x;
    1.24  
    1.25 -
    1.26  (*union of sets represented as lists: no repetitions*)
    1.27  fun xs union [] = xs
    1.28    | [] union ys = ys