equal
deleted
inserted
replaced
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 = |