# HG changeset patch
# User wenzelm
# Date 1526653820 -7200
# Node ID d9f2cf4fc002ac9fc6d362377f5d6efa77163aa0
# Parent  1463c4996fb25f612a65aa537346702081dc5ba7
more exports;

diff -r 1463c4996fb2 -r d9f2cf4fc002 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Thu May 17 19:16:41 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Fri May 18 16:30:20 2018 +0200
@@ -97,6 +97,24 @@
       export_entities "consts" export_const Sign.const_space
         (#constants (Consts.dest (Sign.consts_of thy)));
 
+
+    (* axioms *)
+
+    val encode_axiom =
+      let open XML.Encode Term_XML.Encode
+      in triple (list (pair string sort)) (list (pair string typ)) term end;
+
+    fun export_axiom prop =
+      let
+        val prop' = Logic.unvarify_global prop;
+        val typargs = rev (Term.add_tfrees prop' []);
+        val args = rev (Term.add_frees prop' []);
+      in encode_axiom (typargs, args, prop') end;
+
+    val _ =
+      export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space
+        (Theory.axioms_of thy);
+
     in () end);
 
 end;
diff -r 1463c4996fb2 -r d9f2cf4fc002 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Thu May 17 19:16:41 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Fri May 18 16:30:20 2018 +0200
@@ -54,17 +54,20 @@
 
   /** theory content **/
 
-  sealed case class Theory(
-    name: String, parents: List[String], types: List[Type], consts: List[Const])
+  sealed case class Theory(name: String, parents: List[String],
+    types: List[Type],
+    consts: List[Const],
+    axioms: List[Axiom])
   {
     override def toString: String = name
   }
 
-  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil)
+  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil)
 
   def read_theory(db: SQL.Database, session_name: String, theory_name: String,
     types: Boolean = true,
-    consts: Boolean = true): Theory =
+    consts: Boolean = true,
+    axioms: Boolean = true): Theory =
   {
     val parents =
       Export.read_entry(db, session_name, theory_name, "theory/parents") match {
@@ -77,7 +80,8 @@
       }
     Theory(theory_name, parents,
       if (types) read_types(db, session_name, theory_name) else Nil,
-      if (consts) read_consts(db, session_name, theory_name) else Nil)
+      if (consts) read_consts(db, session_name, theory_name) else Nil,
+      if (axioms) read_axioms(db, session_name, theory_name) else Nil)
   }
 
 
@@ -147,4 +151,27 @@
           }
           Const(entity, args, typ, abbrev)
         })
+
+
+  /* axioms */
+
+  sealed case class Axiom(
+    entity: Entity,
+    typargs: List[(String, Term.Sort)],
+    args: List[(String, Term.Typ)],
+    prop: Term.Term)
+
+  def read_axioms(db: SQL.Database, session_name: String, theory_name: String): List[Axiom] =
+    read_entities(db, session_name, theory_name, "axioms",
+      (tree: XML.Tree) =>
+        {
+          val (entity, body) = decode_entity(tree)
+          val (typargs, args, prop) =
+          {
+            import XML.Decode._
+            import Term_XML.Decode._
+            triple(list(pair(string, sort)), list(pair(string, typ)), term)(body)
+          }
+          Axiom(entity, typargs, args, prop)
+        })
 }