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;