src/Pure/Thy/export_theory.ML
changeset 68232 4b93573ac5b4
parent 68231 0004e7a9fa10
child 68235 a3bd410db5b2
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sun May 20 15:37:16 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sun May 20 16:25:27 2018 +0200
     1.3 @@ -97,23 +97,28 @@
     1.4          (#constants (Consts.dest (Sign.consts_of thy)));
     1.5  
     1.6  
     1.7 -    (* axioms *)
     1.8 +    (* axioms and facts *)
     1.9  
    1.10 -    val encode_axiom =
    1.11 +    val encode_props =
    1.12        let open XML.Encode Term_XML.Encode
    1.13 -      in triple (list (pair string sort)) (list (pair string typ)) term end;
    1.14 +      in triple (list (pair string sort)) (list (pair string typ)) (list term) end;
    1.15  
    1.16 -    fun export_axiom prop =
    1.17 +    fun export_props props =
    1.18        let
    1.19 -        val prop' = Logic.unvarify_global prop;
    1.20 -        val typargs = rev (Term.add_tfrees prop' []);
    1.21 -        val args = rev (Term.add_frees prop' []);
    1.22 -      in encode_axiom (typargs, args, prop') end;
    1.23 +        val props' = map Logic.unvarify_global props;
    1.24 +        val typargs = rev (fold Term.add_tfrees props' []);
    1.25 +        val args = rev (fold Term.add_frees props' []);
    1.26 +      in encode_props (typargs, args, props') end;
    1.27  
    1.28      val _ =
    1.29 -      export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space
    1.30 +      export_entities "axioms" (K (SOME o export_props o single)) Theory.axiom_space
    1.31          (Theory.axioms_of thy);
    1.32  
    1.33 +    val _ =
    1.34 +      export_entities "facts" (K (SOME o export_props o map Thm.full_prop_of))
    1.35 +        (Facts.space_of o Global_Theory.facts_of)
    1.36 +        (Facts.dest_static true [] (Global_Theory.facts_of thy));
    1.37 +
    1.38      in () end);
    1.39  
    1.40  end;