equal
deleted
inserted
replaced
108 val props' = map Logic.unvarify_global props; |
108 val props' = map Logic.unvarify_global props; |
109 val typargs = rev (fold Term.add_tfrees props' []); |
109 val typargs = rev (fold Term.add_tfrees props' []); |
110 val args = rev (fold Term.add_frees props' []); |
110 val args = rev (fold Term.add_frees props' []); |
111 in encode_props (typargs, args, props') end; |
111 in encode_props (typargs, args, props') end; |
112 |
112 |
113 val _ = |
113 val export_axiom = export_props o single; |
114 export_entities "axioms" (K (SOME o export_props o single)) Theory.axiom_space |
114 val export_fact = export_props o Term_Subst.zero_var_indexes_list o map Thm.full_prop_of; |
115 (Theory.axioms_of thy); |
|
116 |
115 |
117 val _ = |
116 val _ = |
118 export_entities "facts" (K (SOME o export_props o map Thm.full_prop_of)) |
117 export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space |
119 (Facts.space_of o Global_Theory.facts_of) |
118 (Theory.axioms_of thy); |
|
119 val _ = |
|
120 export_entities "facts" (K (SOME o export_fact)) (Facts.space_of o Global_Theory.facts_of) |
120 (Facts.dest_static true [] (Global_Theory.facts_of thy)); |
121 (Facts.dest_static true [] (Global_Theory.facts_of thy)); |
121 |
122 |
122 in () end); |
123 in () end); |
123 |
124 |
124 end; |
125 end; |