src/Pure/variable.ML
changeset 77952 27b5cb41c253
parent 74539 f07761ee5a7f
child 77970 31ea5c1f874d
--- 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;