standardize implicit variables: non-zero indexes do occur occasionally, e.g. via RS;
--- a/src/Pure/Thy/export_theory.ML Sun May 20 20:31:40 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML Sun May 20 20:37:11 2018 +0200
@@ -110,13 +110,14 @@
val args = rev (fold Term.add_frees props' []);
in encode_props (typargs, args, props') end;
- val _ =
- export_entities "axioms" (K (SOME o export_props o single)) Theory.axiom_space
- (Theory.axioms_of thy);
+ val export_axiom = export_props o single;
+ val export_fact = export_props o Term_Subst.zero_var_indexes_list o map Thm.full_prop_of;
val _ =
- export_entities "facts" (K (SOME o export_props o map Thm.full_prop_of))
- (Facts.space_of o Global_Theory.facts_of)
+ export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space
+ (Theory.axioms_of thy);
+ val _ =
+ export_entities "facts" (K (SOME o export_fact)) (Facts.space_of o Global_Theory.facts_of)
(Facts.dest_static true [] (Global_Theory.facts_of thy));
in () end);