more compact: avoid redundant entries;

--- a/src/Pure/General/name_space.ML	Wed Apr 12 11:27:11 2023 +0200
+++ b/src/Pure/General/name_space.ML	Wed Apr 12 12:57:10 2023 +0200
@@ -456,7 +456,7 @@
         val restrict = is_some restriction ? filter (fn [_] => false | _ => true);
         val sfxs = restrict (mandatory_suffixes spec);
         val pfxs = restrict (mandatory_prefixes spec);
-      in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end);
+      in apply2 (map Long_Name.implode o distinct op =) (sfxs @ pfxs, sfxs) end);
 
 end;