src/Pure/library.ML
changeset 20348 d59364649bcc
parent 20137 6c04453ac1bd
child 20443 84a624a8f773
     1.1 --- a/src/Pure/library.ML	Mon Aug 07 17:43:51 2006 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Aug 08 08:18:59 2006 +0200
     1.3 @@ -142,7 +142,6 @@
     1.4    val filter: ('a -> bool) -> 'a list -> 'a list
     1.5    val filter_out: ('a -> bool) -> 'a list -> 'a list
     1.6    val map_filter: ('a -> 'b option) -> 'a list -> 'b list
     1.7 -  val equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool
     1.8    val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
     1.9    val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
    1.10    val chop_prefix: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list * ('a list * 'b list)
    1.11 @@ -568,6 +567,12 @@
    1.12  
    1.13  (* basic list functions *)
    1.14  
    1.15 +fun eq_list eq (xs, ys) =
    1.16 +  let
    1.17 +    fun eq' [] [] = true
    1.18 +      | eq' (x :: xs) (y :: ys) = eq (x, y) andalso eq' xs ys
    1.19 +  in length xs = length ys andalso eq' xs ys end;
    1.20 +
    1.21  fun maps f [] = []
    1.22    | maps f (x :: xs) = f x @ maps f xs;
    1.23  
    1.24 @@ -646,10 +651,6 @@
    1.25              | SOME y => SOME (i, y)
    1.26    in get 0 end;
    1.27  
    1.28 -fun eq_list _ ([], []) = true
    1.29 -  | eq_list eq (x :: xs, y :: ys) = eq (x, y) andalso eq_list eq (xs, ys)
    1.30 -  | eq_list _ _ = false;
    1.31 -
    1.32  val flat = List.concat;
    1.33  
    1.34  fun unflat (xs :: xss) ys =
    1.35 @@ -731,12 +732,6 @@
    1.36    [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
    1.37  val split_list = ListPair.unzip;
    1.38  
    1.39 -fun equal_lists eq (xs, ys) =
    1.40 -  let
    1.41 -    fun eq' [] [] = true
    1.42 -      | eq' (x :: xs) (y :: ys) = eq (x, y) andalso eq' xs ys
    1.43 -  in length xs = length ys andalso eq' xs ys end;
    1.44 -
    1.45  
    1.46  (* prefixes, suffixes *)
    1.47  
    1.48 @@ -1034,7 +1029,7 @@
    1.49  fun gen_subset eq (xs, ys) = forall (member eq ys) xs;
    1.50  
    1.51  fun gen_eq_set eq (xs, ys) =
    1.52 -  equal_lists eq (xs, ys) orelse
    1.53 +  eq_list eq (xs, ys) orelse
    1.54      (gen_subset eq (xs, ys) andalso gen_subset (eq o swap) (ys, xs));
    1.55  
    1.56