export facts;

--- a/src/Pure/Thy/export_theory.ML	Sun May 20 15:37:16 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sun May 20 16:25:27 2018 +0200
@@ -97,23 +97,28 @@
         (#constants (Consts.dest (Sign.consts_of thy)));
 
 
-    (* axioms *)
+    (* axioms and facts *)
 
-    val encode_axiom =
+    val encode_props =
       let open XML.Encode Term_XML.Encode
-      in triple (list (pair string sort)) (list (pair string typ)) term end;
+      in triple (list (pair string sort)) (list (pair string typ)) (list term) end;
 
-    fun export_axiom prop =
+    fun export_props props =
       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 props' = map Logic.unvarify_global props;
+        val typargs = rev (fold Term.add_tfrees props' []);
+        val args = rev (fold Term.add_frees props' []);
+      in encode_props (typargs, args, props') end;
 
     val _ =
-      export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space
+      export_entities "axioms" (K (SOME o export_props o single)) Theory.axiom_space
         (Theory.axioms_of thy);
 
+    val _ =
+      export_entities "facts" (K (SOME o export_props o map Thm.full_prop_of))
+        (Facts.space_of o Global_Theory.facts_of)
+        (Facts.dest_static true [] (Global_Theory.facts_of thy));
+
     in () end);
 
 end;

--- a/src/Pure/Thy/export_theory.scala	Sun May 20 15:37:16 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Sun May 20 16:25:27 2018 +0200
@@ -54,17 +54,19 @@
   sealed case class Theory(name: String, parents: List[String],
     types: List[Type],
     consts: List[Const],
-    axioms: List[Axiom])
+    axioms: List[Axiom],
+    facts: List[Fact])
   {
     override def toString: String = name
   }
 
-  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil)
+  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil)
 
   def read_theory(db: SQL.Database, session_name: String, theory_name: String,
     types: Boolean = true,
     consts: Boolean = true,
-    axioms: Boolean = true): Theory =
+    axioms: Boolean = true,
+    facts: Boolean = true): Theory =
   {
     val parents =
       Export.read_entry(db, session_name, theory_name, "theory/parents") match {
@@ -76,7 +78,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 (axioms) read_axioms(db, session_name, theory_name) else Nil)
+      if (axioms) read_axioms(db, session_name, theory_name) else Nil,
+      if (facts) read_facts(db, session_name, theory_name) else Nil)
   }
 
 
@@ -148,7 +151,15 @@
         })
 
 
-  /* axioms */
+  /* axioms and facts */
+
+  def decode_props(body: XML.Body):
+    (List[(String, Term.Sort)], List[(String, Term.Typ)], List[Term.Term]) =
+  {
+    import XML.Decode._
+    import Term_XML.Decode._
+    triple(list(pair(string, sort)), list(pair(string, typ)), list(term))(body)
+  }
 
   sealed case class Axiom(
     entity: Entity,
@@ -161,12 +172,22 @@
       (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)
-          }
+          val (typargs, args, List(prop)) = decode_props(body)
           Axiom(entity, typargs, args, prop)
         })
+
+  sealed case class Fact(
+    entity: Entity,
+    typargs: List[(String, Term.Sort)],
+    args: List[(String, Term.Typ)],
+    props: List[Term.Term])
+
+  def read_facts(db: SQL.Database, session_name: String, theory_name: String): List[Fact] =
+    read_entities(db, session_name, theory_name, "facts",
+      (tree: XML.Tree) =>
+        {
+          val (entity, body) = decode_entity(tree)
+          val (typargs, args, props) = decode_props(body)
+          Fact(entity, typargs, args, props)
+        })
 }