equal
deleted
inserted
replaced
160 |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx')); |
160 |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx')); |
161 val lhs = Term.list_comb (const, params); |
161 val lhs = Term.list_comb (const, params); |
162 |
162 |
163 val ((_, def), lthy3) = lthy2 |
163 val ((_, def), lthy3) = lthy2 |
164 |> Local_Theory.background_theory_result |
164 |> Local_Theory.background_theory_result |
165 (Thm.add_def lthy2 false false |
165 (Thm.add_def (Proof_Context.defs_context lthy2) false false |
166 (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs))); |
166 (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs))); |
167 in ((lhs, def), lthy3) end; |
167 in ((lhs, def), lthy3) end; |
168 |
168 |
169 fun background_declaration decl lthy = |
169 fun background_declaration decl lthy = |
170 let |
170 let |