equal
deleted
inserted
replaced
283 |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax |
283 |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax |
284 |-> (fn (param_map, params, assm_axiom) => |
284 |-> (fn (param_map, params, assm_axiom) => |
285 `(fn thy => calculate thy class sups base_sort param_map assm_axiom) |
285 `(fn thy => calculate thy class sups base_sort param_map assm_axiom) |
286 #-> (fn (base_morph, morph, export_morph, axiom, assm_intro, of_class) => |
286 #-> (fn (base_morph, morph, export_morph, axiom, assm_intro, of_class) => |
287 Locale.add_registration (class, (morph, export_morph)) |
287 Locale.add_registration (class, (morph, export_morph)) |
288 #> Locale.activate_global_facts (class, morph $> export_morph) |
288 #> Context.theory_map (Locale.activate_facts (class, morph $> export_morph)) |
289 #> register class sups params base_sort base_morph axiom assm_intro of_class)) |
289 #> register class sups params base_sort base_morph axiom assm_intro of_class)) |
290 |> TheoryTarget.init (SOME class) |
290 |> TheoryTarget.init (SOME class) |
291 |> pair class |
291 |> pair class |
292 end; |
292 end; |
293 |
293 |