85 fun make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), |
85 fun make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), |
86 (defs, operations)) = |
86 (defs, operations)) = |
87 Class_Data {consts = consts, base_sort = base_sort, |
87 Class_Data {consts = consts, base_sort = base_sort, |
88 base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, |
88 base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, |
89 of_class = of_class, axiom = axiom, defs = defs, operations = operations}; |
89 of_class = of_class, axiom = axiom, defs = defs, operations = operations}; |
|
90 |
90 fun map_class_data f (Class_Data {consts, base_sort, base_morph, export_morph, assm_intro, |
91 fun map_class_data f (Class_Data {consts, base_sort, base_morph, export_morph, assm_intro, |
91 of_class, axiom, defs, operations}) = |
92 of_class, axiom, defs, operations}) = |
92 make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), |
93 make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), |
93 (defs, operations))); |
94 (defs, operations))); |
|
95 |
94 fun merge_class_data _ (Class_Data {consts = consts, |
96 fun merge_class_data _ (Class_Data {consts = consts, |
95 base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, |
97 base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, |
96 of_class = of_class, axiom = axiom, defs = defs1, operations = operations1}, |
98 of_class = of_class, axiom = axiom, defs = defs1, operations = operations1}, |
97 Class_Data {consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _, |
99 Class_Data {consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _, |
98 of_class = _, axiom = _, defs = defs2, operations = operations2}) = |
100 of_class = _, axiom = _, defs = defs2, operations = operations2}) = |