src/Pure/Thy/export_theory.ML
changeset 68208 d9f2cf4fc002
parent 68206 dedf1a70d1fa
child 68230 9bee37c2ac2b
     1.1 --- a/src/Pure/Thy/export_theory.ML	Thu May 17 19:16:41 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Fri May 18 16:30:20 2018 +0200
     1.3 @@ -97,6 +97,24 @@
     1.4        export_entities "consts" export_const Sign.const_space
     1.5          (#constants (Consts.dest (Sign.consts_of thy)));
     1.6  
     1.7 +
     1.8 +    (* axioms *)
     1.9 +
    1.10 +    val encode_axiom =
    1.11 +      let open XML.Encode Term_XML.Encode
    1.12 +      in triple (list (pair string sort)) (list (pair string typ)) term end;
    1.13 +
    1.14 +    fun export_axiom prop =
    1.15 +      let
    1.16 +        val prop' = Logic.unvarify_global prop;
    1.17 +        val typargs = rev (Term.add_tfrees prop' []);
    1.18 +        val args = rev (Term.add_frees prop' []);
    1.19 +      in encode_axiom (typargs, args, prop') end;
    1.20 +
    1.21 +    val _ =
    1.22 +      export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space
    1.23 +        (Theory.axioms_of thy);
    1.24 +
    1.25      in () end);
    1.26  
    1.27  end;