291 |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax |
291 |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax |
292 ||> Theory.checkpoint |
292 ||> Theory.checkpoint |
293 |-> (fn (param_map, params, assm_axiom) => |
293 |-> (fn (param_map, params, assm_axiom) => |
294 `(fn thy => calculate thy class sups base_sort param_map assm_axiom) |
294 `(fn thy => calculate thy class sups base_sort param_map assm_axiom) |
295 #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) => |
295 #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) => |
296 Locale.add_registration (class, base_morph) |
296 Locale.add_registration (class, case eq_morph of SOME eq_morph => base_morph $> eq_morph | NONE => base_morph) |
|
297 (*FIXME should avoid modification of base morphism, but then problem with sublocale linorder < distrib_lattice*) |
297 (Option.map (rpair true) eq_morph) export_morph |
298 (Option.map (rpair true) eq_morph) export_morph |
298 #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class)) |
299 #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class)) |
299 |> Theory_Target.init (SOME class) |
300 |> Theory_Target.init (SOME class) |
300 |> pair class |
301 |> pair class |
301 end; |
302 end; |