equal
deleted
inserted
replaced
55 val get_bundle = get_bundle_generic o Context.Proof; |
55 val get_bundle = get_bundle_generic o Context.Proof; |
56 fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt; |
56 fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt; |
57 |
57 |
58 fun define_bundle (b, bundle) context = |
58 fun define_bundle (b, bundle) context = |
59 let |
59 let |
60 val bundle' = Attrib.trim_context bundle; |
60 val bundle' = Attrib.trim_context_thms bundle; |
61 val (name, bundles') = Name_Space.define context true (b, bundle') (get_bundles_generic context); |
61 val (name, bundles') = Name_Space.define context true (b, bundle') (get_bundles_generic context); |
62 val context' = (Data.map o apfst o K) bundles' context; |
62 val context' = (Data.map o apfst o K) bundles' context; |
63 in (name, context') end; |
63 in (name, context') end; |
64 |
64 |
65 |
65 |
69 (case #2 (Data.get (Context.Theory thy)) of |
69 (case #2 (Data.get (Context.Theory thy)) of |
70 SOME thms => thms |
70 SOME thms => thms |
71 | NONE => error "Missing bundle target"); |
71 | NONE => error "Missing bundle target"); |
72 |
72 |
73 val reset_target = (Context.theory_map o Data.map o apsnd o K) NONE; |
73 val reset_target = (Context.theory_map o Data.map o apsnd o K) NONE; |
74 val set_target = Context.theory_map o Data.map o apsnd o K o SOME o Attrib.trim_context; |
74 val set_target = Context.theory_map o Data.map o apsnd o K o SOME o Attrib.trim_context_thms; |
75 |
75 |
76 fun augment_target thms = |
76 fun augment_target thms = |
77 Local_Theory.background_theory (fn thy => set_target (the_target thy @ thms) thy); |
77 Local_Theory.background_theory (fn thy => set_target (the_target thy @ thms) thy); |
78 |
78 |
79 |
79 |