src/Pure/variable.ML
changeset 77952 27b5cb41c253
parent 74539 f07761ee5a7f
child 77970 31ea5c1f874d
equal deleted inserted replaced
77951:6c8682291a5d 77952:27b5cb41c253
   431         |> Context_Position.set_visible_generic false;
   431         |> Context_Position.set_visible_generic false;
   432     in
   432     in
   433       ctxt
   433       ctxt
   434       |> map_fixes
   434       |> map_fixes
   435         (Name_Space.define context true (Binding.make (x', pos), (x, proper)) #> snd #>
   435         (Name_Space.define context true (Binding.make (x', pos), (x, proper)) #> snd #>
   436           Name_Space.alias_table Name_Space.global_naming (Binding.make (x, pos)) x')
   436           x <> "" ? Name_Space.alias_table Name_Space.global_naming (Binding.make (x, pos)) x')
   437       |> declare_fixed x
   437       |> declare_fixed x
   438       |> declare_constraints (Syntax.free x')
   438       |> declare_constraints (Syntax.free x')
   439   end;
   439   end;
   440 
   440 
   441 fun new_fixes names' args =
   441 fun new_fixes names' args =