src/Pure/library.ML
changeset 19119 dea8d858d37f
parent 19046 bc5c6c9b114e
child 19233 77ca20b0ed77
     1.1 --- a/src/Pure/library.ML	Tue Feb 21 16:37:54 2006 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Feb 22 10:18:17 2006 +0100
     1.3 @@ -221,11 +221,8 @@
     1.4  
     1.5    (*lists as tables -- see also Pure/General/alist.ML*)
     1.6    val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
     1.7 -  val gen_merge_lists': ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
     1.8    val merge_lists: ''a list -> ''a list -> ''a list
     1.9 -  val merge_lists': ''a list -> ''a list -> ''a list
    1.10    val merge_alists: (''a * 'b) list -> (''a * 'b) list -> (''a * 'b) list
    1.11 -  val merge_alists': (''a * 'b) list -> (''a * 'b) list -> (''a * 'b) list
    1.12  
    1.13    (*balanced trees*)
    1.14    exception Balance
    1.15 @@ -1043,24 +1040,14 @@
    1.16    in dups end;
    1.17  
    1.18  
    1.19 -
    1.20 -(** association lists **)
    1.21 -
    1.22 -(* lists as tables -- legacy operations *)
    1.23 +(** association lists -- legacy operations **)
    1.24  
    1.25  fun gen_merge_lists _ xs [] = xs
    1.26    | gen_merge_lists _ [] ys = ys
    1.27    | gen_merge_lists eq xs ys = xs @ gen_rems eq (ys, xs);
    1.28  
    1.29 -fun gen_merge_lists' _ xs [] = xs
    1.30 -  | gen_merge_lists' _ [] ys = ys
    1.31 -  | gen_merge_lists' eq xs ys = gen_rems eq (ys, xs) @ xs;
    1.32 -
    1.33  fun merge_lists xs ys = gen_merge_lists (op =) xs ys;
    1.34 -fun merge_lists' xs ys = gen_merge_lists' (op =) xs ys;
    1.35  fun merge_alists al = gen_merge_lists (eq_fst (op =)) al;
    1.36 -fun merge_alists' al = gen_merge_lists' (eq_fst (op =)) al;
    1.37 -
    1.38  
    1.39  
    1.40  (** balanced trees **)