138 ctxt |
138 ctxt |
139 |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false)) |
139 |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false)) |
140 end |
140 end |
141 |
141 |
142 fun define_overloaded (c, U) (v, checked) (b_def, rhs) = |
142 fun define_overloaded (c, U) (v, checked) (b_def, rhs) = |
143 Local_Theory.theory_result |
143 Local_Theory.background_theory_result |
144 (Thm.add_def (not checked) true (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs))) |
144 (Thm.add_def (not checked) true (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs))) |
145 ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v)) |
145 ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v)) |
146 ##> Local_Theory.target synchronize_syntax |
146 ##> Local_Theory.target synchronize_syntax |
147 #-> (fn (_, def) => pair (Const (c, U), def)) |
147 #-> (fn (_, def) => pair (Const (c, U), def)) |
148 |
148 |