--- a/src/Pure/library.ML Thu May 04 23:30:59 2023 +0200
+++ b/src/Pure/library.ML Fri May 05 11:29:27 2023 +0200
@@ -371,12 +371,21 @@
(* basic list functions *)
-fun eq_list eq (list1, list2) =
- pointer_eq (list1, list2) orelse
- let
- fun eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys)
- | eq_lst _ = true;
- in length list1 = length list2 andalso eq_lst (list1, list2) end;
+fun eq_list eq lists =
+ let
+ fun eq_len args =
+ pointer_eq args orelse
+ (case args of
+ (_ :: xs, _ :: ys) => eq_len (xs, ys)
+ | ([], []) => true
+ | _ => false);
+ fun eq_lst args =
+ pointer_eq args orelse
+ (case args of
+ (x :: xs, y :: ys) => eq (x, y) andalso eq_lst (xs, ys)
+ | ([], []) => true
+ | _ => false);
+ in eq_len lists andalso eq_lst lists end;
fun maps f [] = []
| maps f (x :: xs) = f x @ maps f xs;