src/Pure/library.ML
changeset 77959 8d905eef9feb
parent 77912 430e6c477ba4
child 77963 3a97b5bff51a
--- a/src/Pure/library.ML	Wed May 03 11:34:47 2023 +0200
+++ b/src/Pure/library.ML	Wed May 03 23:11:12 2023 +0200
@@ -607,9 +607,8 @@
       else ([], (xs, ys));
 
 fun prefixes1 [] = []
-  | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
-
-fun prefixes xs = [] :: prefixes1 xs;
+  | prefixes1 (x :: xs) = map (cons x) (prefixes xs)
+and prefixes xs = [] :: prefixes1 xs;
 
 fun suffixes1 xs = map rev (prefixes1 (rev xs));
 fun suffixes xs = [] :: suffixes1 xs;