# HG changeset patch
# User wenzelm
# Date 1683148272 -7200
# Node ID 8d905eef9feba1515212435f5d14bb2205215cf0
# Parent  d7eabea9f837c1efbedd1ac98b8dbd0994e94f74
tuned;

diff -r d7eabea9f837 -r 8d905eef9feb src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed May 03 11:34:47 2023 +0200
+++ b/src/Pure/General/name_space.ML	Wed May 03 23:11:12 2023 +0200
@@ -153,10 +153,10 @@
 
 fun mandatory xs = fold_rev (fn (x, b) => b ? cons x) xs [];
 
-fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs
-and mandatory_prefixes1 [] = []
+fun mandatory_prefixes1 [] = []
   | mandatory_prefixes1 ((x, true) :: xs) = map (cons x) (mandatory_prefixes1 xs)
-  | mandatory_prefixes1 ((x, false) :: xs) = map (cons x) (mandatory_prefixes xs);
+  | mandatory_prefixes1 ((x, false) :: xs) = map (cons x) (mandatory_prefixes xs)
+and mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs
 
 fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
 
diff -r d7eabea9f837 -r 8d905eef9feb src/Pure/library.ML
--- 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;