# HG changeset patch
# User wenzelm
# Date 1681297030 -7200
# Node ID b2b985d8a93d2d73e25cf0ecdb1ac3e30701be91
# Parent  29146fb57e791fc6243bbe3960c8d90f24e038b5
more compact: avoid redundant entries;

diff -r 29146fb57e79 -r b2b985d8a93d src/Pure/General/name_space.ML
--- 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;