325 |> snd |> Local_Theory.exit_global |
325 |> snd |> Local_Theory.exit_global |
326 |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax |
326 |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax |
327 |-> (fn (param_map, params, assm_axiom) => |
327 |-> (fn (param_map, params, assm_axiom) => |
328 `(fn thy => calculate thy class sups base_sort param_map assm_axiom) |
328 `(fn thy => calculate thy class sups base_sort param_map assm_axiom) |
329 #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) => |
329 #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) => |
330 Locale.add_registration_theory |
330 Locale.add_registration_theory' |
331 {inst = (class, base_morph), |
331 {inst = (class, base_morph), |
332 mixin = Option.map (rpair true) eq_morph, |
332 mixin = Option.map (rpair true) eq_morph, |
333 export = export_morph} |
333 export = export_morph} |
334 #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class |
334 #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class |
335 #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class))) |
335 #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class))) |