# HG changeset patch
# User wenzelm
# Date 1681291550 -7200
# Node ID 56d7da3e79feaa6a76e447b6455ee4d0b02fb377
# Parent  9d124714a9e85599e5a5f43d1b7583c28bef4702
tuned;

diff -r 9d124714a9e8 -r 56d7da3e79fe src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Apr 12 10:52:50 2023 +0200
+++ b/src/Pure/General/name_space.ML	Wed Apr 12 11:25:50 2023 +0200
@@ -435,7 +435,7 @@
 
 (* accesses *)
 
-fun mandatory xs = map_filter (fn (x, true) => SOME x | _ => NONE) xs;
+fun mandatory xs = fold_rev (fn (x, b) => b ? cons x) xs [];
 
 fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs
 and mandatory_prefixes1 [] = []