95 val _ = |
95 val _ = |
96 export_entities "consts" export_const Sign.const_space |
96 export_entities "consts" export_const Sign.const_space |
97 (#constants (Consts.dest (Sign.consts_of thy))); |
97 (#constants (Consts.dest (Sign.consts_of thy))); |
98 |
98 |
99 |
99 |
100 (* axioms *) |
100 (* axioms and facts *) |
101 |
101 |
102 val encode_axiom = |
102 val encode_props = |
103 let open XML.Encode Term_XML.Encode |
103 let open XML.Encode Term_XML.Encode |
104 in triple (list (pair string sort)) (list (pair string typ)) term end; |
104 in triple (list (pair string sort)) (list (pair string typ)) (list term) end; |
105 |
105 |
106 fun export_axiom prop = |
106 fun export_props props = |
107 let |
107 let |
108 val prop' = Logic.unvarify_global prop; |
108 val props' = map Logic.unvarify_global props; |
109 val typargs = rev (Term.add_tfrees prop' []); |
109 val typargs = rev (fold Term.add_tfrees props' []); |
110 val args = rev (Term.add_frees prop' []); |
110 val args = rev (fold Term.add_frees props' []); |
111 in encode_axiom (typargs, args, prop') end; |
111 in encode_props (typargs, args, props') end; |
112 |
112 |
113 val _ = |
113 val _ = |
114 export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space |
114 export_entities "axioms" (K (SOME o export_props o single)) Theory.axiom_space |
115 (Theory.axioms_of thy); |
115 (Theory.axioms_of thy); |
|
116 |
|
117 val _ = |
|
118 export_entities "facts" (K (SOME o export_props o map Thm.full_prop_of)) |
|
119 (Facts.space_of o Global_Theory.facts_of) |
|
120 (Facts.dest_static true [] (Global_Theory.facts_of thy)); |
116 |
121 |
117 in () end); |
122 in () end); |
118 |
123 |
119 end; |
124 end; |