153 Local_Theory.background_theory_result |
153 Local_Theory.background_theory_result |
154 (Thm.add_def_global (not checked) true |
154 (Thm.add_def_global (not checked) true |
155 (Thm.def_binding_optional (Binding.name v) b_def, |
155 (Thm.def_binding_optional (Binding.name v) b_def, |
156 Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs))) |
156 Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs))) |
157 ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v)) |
157 ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v)) |
158 ##> Local_Theory.target synchronize_syntax |
158 ##> Local_Theory.map_contexts synchronize_syntax |
159 #-> (fn (_, def) => pair (Const (c, U), def)); |
159 #-> (fn (_, def) => pair (Const (c, U), def)); |
160 |
160 |
161 fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = |
161 fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = |
162 (case operation lthy b of |
162 (case operation lthy b of |
163 SOME (c, (v, checked)) => |
163 SOME (c, (v, checked)) => |