623 fun init_context f x = Toplevel.init_theory (fn _ => fetch_context f x) (K ()) (K ()); |
623 fun init_context f x = Toplevel.init_theory (fn _ => fetch_context f x) (K ()) (K ()); |
624 |
624 |
625 val context = init_context (ThyInfo.quiet_update_thy true); |
625 val context = init_context (ThyInfo.quiet_update_thy true); |
626 |
626 |
627 |
627 |
628 (* global locale registration *) |
628 (* global registration of locale interpretation *) |
629 |
629 |
630 fun register_globally (((prfx, atts), expr), insts) b (* bool *) thy = |
630 fun register_globally (((prfx, atts), expr), insts) b (* bool *) thy = |
631 let |
631 let |
632 val (thy', propss, activate) = |
632 val (thy', propss, activate) = Locale.prep_registration |
633 Locale.prep_registration (prfx, []) expr insts thy; |
633 (prfx, map (Attrib.global_attribute thy) atts) expr insts thy; |
634 (* TODO: convert atts *) |
634 fun witness id (thy, thm) = let |
635 fun register id (thy, thm) = let |
|
636 val thm' = Drule.freeze_all thm; |
635 val thm' = Drule.freeze_all thm; |
637 in |
636 in |
638 (Locale.global_activate_thm id thm' thy, thm') |
637 (Locale.global_add_witness id thm' thy, thm') |
639 end; |
638 end; |
640 in |
639 in |
641 multi_theorem_i Drule.internalK activate ("", []) [] |
640 multi_theorem_i Drule.internalK activate ("", []) [] |
642 (map (fn (id as (n, _), props) => ((NameSpace.base n, [register id]), |
641 (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]), |
643 map (fn prop => (prop, ([], []))) props)) propss) b thy' |
642 map (fn prop => (prop, ([], []))) props)) propss) b thy' |
644 end; |
643 end; |
645 |
644 |
646 |
645 |
647 end; |
646 end; |