src/Pure/Thy/export_theory.ML
changeset 68235 a3bd410db5b2
parent 68232 4b93573ac5b4
child 68264 bb9a3be6952a
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sun May 20 20:31:40 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sun May 20 20:37:11 2018 +0200
     1.3 @@ -110,13 +110,14 @@
     1.4          val args = rev (fold Term.add_frees props' []);
     1.5        in encode_props (typargs, args, props') end;
     1.6  
     1.7 -    val _ =
     1.8 -      export_entities "axioms" (K (SOME o export_props o single)) Theory.axiom_space
     1.9 -        (Theory.axioms_of thy);
    1.10 +    val export_axiom = export_props o single;
    1.11 +    val export_fact = export_props o Term_Subst.zero_var_indexes_list o map Thm.full_prop_of;
    1.12  
    1.13      val _ =
    1.14 -      export_entities "facts" (K (SOME o export_props o map Thm.full_prop_of))
    1.15 -        (Facts.space_of o Global_Theory.facts_of)
    1.16 +      export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space
    1.17 +        (Theory.axioms_of thy);
    1.18 +    val _ =
    1.19 +      export_entities "facts" (K (SOME o export_fact)) (Facts.space_of o Global_Theory.facts_of)
    1.20          (Facts.dest_static true [] (Global_Theory.facts_of thy));
    1.21  
    1.22      in () end);