diff -r 01e04f024bb5 -r 3a97b5bff51a src/Pure/library.ML
--- 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;