# HG changeset patch
# User wenzelm
# Date 1526841431 -7200
# Node ID a3bd410db5b21ed1397862eb4bf0599f2d67a1de
# Parent  07eb13eb40657875d8c3c86e53be64cac34295de
standardize implicit variables: non-zero indexes do occur occasionally, e.g. via RS;

diff -r 07eb13eb4065 -r a3bd410db5b2 src/Pure/Thy/export_theory.ML
--- 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);