equal
deleted
inserted
replaced
288 |> adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax |
288 |> adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax |
289 ||> Theory.checkpoint |
289 ||> Theory.checkpoint |
290 |-> (fn (param_map, params, assm_axiom) => |
290 |-> (fn (param_map, params, assm_axiom) => |
291 `(fn thy => calculate thy class sups base_sort param_map assm_axiom) |
291 `(fn thy => calculate thy class sups base_sort param_map assm_axiom) |
292 #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) => |
292 #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) => |
293 Locale.add_registration (class, base_morph $> eq_morph) NONE export_morph |
293 Locale.add_registration (class, base_morph $> eq_morph (*FIXME duplication*)) (SOME (eq_morph, true)) export_morph |
294 (*FIXME should not modify base_morph, although admissible*) |
|
295 #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class)) |
294 #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class)) |
296 |> Theory_Target.init (SOME class) |
295 |> Theory_Target.init (SOME class) |
297 |> pair class |
296 |> pair class |
298 end; |
297 end; |
299 |
298 |