63 |
63 |
64 fun define_mixins [] expr_ctxt = ([], expr_ctxt) |
64 fun define_mixins [] expr_ctxt = ([], expr_ctxt) |
65 (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*) |
65 (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*) |
66 | define_mixins pre_defs expr_lthy = |
66 | define_mixins pre_defs expr_lthy = |
67 let |
67 let |
68 val (defs, forked_lthy) = fold_map Local_Theory.define pre_defs expr_lthy; |
68 val ((_, defs), inner_def_lthy) = |
|
69 expr_lthy |
|
70 |> Local_Theory.open_target |
|
71 ||>> fold_map Local_Theory.define pre_defs |
69 val def_lthy = |
72 val def_lthy = |
70 Proof_Context.transfer (Proof_Context.theory_of forked_lthy) expr_lthy; |
73 inner_def_lthy |
71 val def_eqns = defs |
74 |> Local_Theory.close_target; |
72 |> map (Thm.symmetric o |
75 val def_eqns = |
73 Morphism.thm (Local_Theory.standard_morphism forked_lthy def_lthy) o snd o snd); |
76 defs |
74 in (def_eqns, def_lthy) end; |
77 |> map (Thm.symmetric o snd o snd) |
|
78 |> Proof_Context.export inner_def_lthy def_lthy; |
|
79 in (def_eqns, Proof_Context.transfer (Proof_Context.theory_of def_lthy) expr_lthy) end; |
75 |
80 |
76 fun prep_interpretation prep_expr prep_term prep_prop prep_attr |
81 fun prep_interpretation prep_expr prep_term prep_prop prep_attr |
77 expression raw_defs raw_eqns initial_ctxt = |
82 expression raw_defs raw_eqns initial_ctxt = |
78 let |
83 let |
79 val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt; |
84 val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt; |