44 atomize_rulify: thm list * thm list}; |
44 atomize_rulify: thm list * thm list}; |
45 |
45 |
46 fun make_data (base_sort, judgment, atomize_rulify) = |
46 fun make_data (base_sort, judgment, atomize_rulify) = |
47 Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify}; |
47 Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify}; |
48 |
48 |
49 structure ObjectLogicData = Theory_Data |
49 structure Data = Theory_Data |
50 ( |
50 ( |
51 type T = data; |
51 type T = data; |
52 val empty = make_data (NONE, NONE, ([], [])); |
52 val empty = make_data (NONE, NONE, ([], [])); |
53 val extend = I; |
53 val extend = I; |
54 |
54 |
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), |
63 (Thm.merge_thms (atomize1, atomize2), Thm.merge_thms (rulify1, rulify2))); |
63 (Thm.merge_thms (atomize1, atomize2), Thm.merge_thms (rulify1, rulify2))); |
64 ); |
64 ); |
65 |
65 |
66 fun map_data f = ObjectLogicData.map (fn (Data {base_sort, judgment, atomize_rulify}) => |
66 fun map_data f = Data.map (fn (Data {base_sort, judgment, atomize_rulify}) => |
67 make_data (f (base_sort, judgment, atomize_rulify))); |
67 make_data (f (base_sort, judgment, atomize_rulify))); |
68 |
68 |
69 fun get_data thy = ObjectLogicData.get thy |> (fn Data args => args); |
69 fun get_data thy = Data.get thy |> (fn Data args => args); |
70 |
70 |
71 |
71 |
72 |
72 |
73 (** generic treatment of judgments -- with a single argument only **) |
73 (** generic treatment of judgments -- with a single argument only **) |
74 |
74 |