tuned;

--- a/src/Pure/General/long_name.ML	Wed Dec 20 12:50:33 2023 +0100
+++ b/src/Pure/General/long_name.ML	Wed Dec 20 12:50:38 2023 +0100
@@ -75,7 +75,7 @@
 fun count "" = 0
   | count name = String.fold (fn c => c = separator_char ? Integer.add 1) name 1;
 
-val hidden_prefix = "??."
+val hidden_prefix = "??.";
 val hidden = prefix hidden_prefix;
 val is_hidden = String.isPrefix hidden_prefix;
 val dest_hidden = try (unprefix hidden_prefix);