58 in (Thm.symmetric def, lthy'') end; |
58 in (Thm.symmetric def, lthy'') end; |
59 |
59 |
60 fun augment_with_defs _ [] _ = pair [] |
60 fun augment_with_defs _ [] _ = pair [] |
61 (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*) |
61 (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*) |
62 | augment_with_defs prep_term raw_defs deps = |
62 | augment_with_defs prep_term raw_defs deps = |
63 Local_Theory.subtarget_result Morphism.fact |
63 Local_Theory.begin_nested |
64 (fold Locale.activate_declarations deps |
64 #> snd |
65 #> fold_map (augment_with_def prep_term) raw_defs); |
65 #> fold Locale.activate_declarations deps |
|
66 #> fold_map (augment_with_def prep_term) raw_defs |
|
67 #> Local_Theory.end_nested_result Morphism.fact; |
66 |
68 |
67 fun prep_interpretation prep_expr prep_term |
69 fun prep_interpretation prep_expr prep_term |
68 expression raw_defs initial_ctxt = |
70 expression raw_defs initial_ctxt = |
69 let |
71 let |
70 val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt; |
72 val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt; |