52 val empty = make_data (NONE, NONE, ([], [])); |
52 val empty = make_data (NONE, NONE, ([], [])); |
53 val extend = I; |
53 val extend = I; |
54 |
54 |
55 fun merge_opt eq (SOME x, SOME y) = |
55 fun merge_opt eq (SOME x, SOME y) = |
56 if eq (x, y) then SOME x else error "Attempt to merge different object-logics" |
56 if eq (x, y) then SOME x else error "Attempt to merge different object-logics" |
57 | merge_opt _ (x, y) = if is_some x then x else y; |
57 | merge_opt _ data = merge_options data; |
58 |
58 |
59 fun merge |
59 fun merge |
60 (Data {base_sort = base_sort1, judgment = judgment1, atomize_rulify = (atomize1, rulify1)}, |
60 (Data {base_sort = base_sort1, judgment = judgment1, atomize_rulify = (atomize1, rulify1)}, |
61 Data {base_sort = base_sort2, judgment = judgment2, atomize_rulify = (atomize2, rulify2)}) = |
61 Data {base_sort = base_sort2, judgment = judgment2, atomize_rulify = (atomize2, rulify2)}) = |
62 make_data (merge_opt (op =) (base_sort1, base_sort2), merge_opt (op =) (judgment1, judgment2), |
62 make_data (merge_opt (op =) (base_sort1, base_sort2), merge_opt (op =) (judgment1, judgment2), |