# HG changeset patch
# User wenzelm
# Date 1683018679 -7200
# Node ID 27b5cb41c253567ff0c272118197d7c94102065f
# Parent  6c8682291a5d827db5bf0cb48c70880c20eec260
proper checks;

diff -r 6c8682291a5d -r 27b5cb41c253 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue May 02 10:49:38 2023 +0200
+++ b/src/Pure/General/name_space.ML	Tue May 02 11:11:19 2023 +0200
@@ -546,6 +546,8 @@
       val _ = the_entry space name;
       val name_spec as {full_name = alias_name, ...} = name_spec naming binding;
       val more_accs = make_accesses name_spec;
+      val _ = alias_name = "" andalso error (Binding.bad binding);
+
       val internals' = internals |> fold (add_name name) more_accs;
       val externals' = externals
         |> Change_Table.map_entry name (fn {accesses, aliases, entry} =>
diff -r 6c8682291a5d -r 27b5cb41c253 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Tue May 02 10:49:38 2023 +0200
+++ b/src/Pure/variable.ML	Tue May 02 11:11:19 2023 +0200
@@ -433,7 +433,7 @@
       ctxt
       |> map_fixes
         (Name_Space.define context true (Binding.make (x', pos), (x, proper)) #> snd #>
-          Name_Space.alias_table Name_Space.global_naming (Binding.make (x, pos)) x')
+          x <> "" ? Name_Space.alias_table Name_Space.global_naming (Binding.make (x, pos)) x')
       |> declare_fixed x
       |> declare_constraints (Syntax.free x')
   end;