clarified export of axioms and theorems (identified derivations instead of projected facts);

--- a/src/Pure/Thy/export_theory.ML	Mon Aug 19 20:08:12 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Mon Aug 19 21:23:13 2019 +0200
@@ -218,7 +218,7 @@
         (#constants (Consts.dest (Sign.consts_of thy)));
 
 
-    (* axioms and facts *)
+    (* axioms *)
 
     fun standard_prop used extra_shyps raw_prop raw_proof =
       let
@@ -236,12 +236,26 @@
     fun encode_axiom used prop =
       encode_prop (#1 (standard_prop used [] prop NONE));
 
+    val _ =
+      export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t))
+        Theory.axiom_space (Theory.axioms_of thy);
+
+
+    (* theorems *)
+
     val clean_thm =
       Thm.transfer thy
       #> Thm.check_hyps (Context.Theory thy)
       #> Thm.strip_shyps;
 
-    val encode_fact = clean_thm #> (fn thm =>
+    fun entity_markup_thm (serial, (name, i)) =
+      let
+        val space = Facts.space_of (Global_Theory.facts_of thy);
+        val xname = Name_Space.extern_shortest thy_ctxt space name;
+        val {pos, ...} = Name_Space.the_entry space name;
+      in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end;
+
+    val encode_thm = clean_thm #> (fn thm =>
       standard_prop Name.context
         (Thm.extra_shyps thm)
         (Thm.full_prop_of thm)
@@ -249,13 +263,16 @@
       let open XML.Encode Term_XML.Encode
       in pair encode_prop (option Proofterm.encode_full) end);
 
-    val _ =
-      export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t))
-        Theory.axiom_space (Theory.axioms_of thy);
-    val _ =
-      export_entities "facts" (K (SOME o XML.Encode.list encode_fact))
-        (Facts.space_of o Global_Theory.facts_of)
-        (Facts.dest_static true [] (Global_Theory.facts_of thy));
+    fun export_thms thms =
+      let val elems =
+        thms |> map (fn (serial, thm_name) =>
+          let
+            val markup = entity_markup_thm (serial, thm_name);
+            val body = encode_thm (Global_Theory.get_thm_name thy (thm_name, Position.none));
+          in XML.Elem (markup, body) end)
+      in if null elems then () else export_body thy "thms" elems end;
+
+    val _ = export_thms (Global_Theory.dest_thm_names thy);
 
 
     (* type classes *)

--- a/src/Pure/Thy/export_theory.scala	Mon Aug 19 20:08:12 2019 +0200
+++ b/src/Pure/Thy/export_theory.scala	Mon Aug 19 21:23:13 2019 +0200
@@ -28,7 +28,7 @@
     types: Boolean = true,
     consts: Boolean = true,
     axioms: Boolean = true,
-    facts: Boolean = true,
+    thms: Boolean = true,
     classes: Boolean = true,
     locales: Boolean = true,
     locale_dependencies: Boolean = true,
@@ -44,7 +44,7 @@
           Export.read_theory_names(db, session_name).map((theory_name: String) =>
             read_theory(Export.Provider.database(db, session_name, theory_name),
               session_name, theory_name, types = types, consts = consts,
-              axioms = axioms, facts = facts, classes = classes, locales = locales,
+              axioms = axioms, thms = thms, classes = classes, locales = locales,
               locale_dependencies = locale_dependencies, classrel = classrel, arities = arities,
               typedefs = typedefs, cache = Some(cache)))
         }
@@ -70,8 +70,8 @@
   sealed case class Theory(name: String, parents: List[String],
     types: List[Type],
     consts: List[Const],
-    axioms: List[Fact_Single],
-    facts: List[Fact_Multi],
+    axioms: List[Axiom],
+    thms: List[Thm],
     classes: List[Class],
     locales: List[Locale],
     locale_dependencies: List[Locale_Dependency],
@@ -86,7 +86,7 @@
         types.iterator.map(_.entity.serial) ++
         consts.iterator.map(_.entity.serial) ++
         axioms.iterator.map(_.entity.serial) ++
-        facts.iterator.map(_.entity.serial) ++
+        thms.iterator.map(_.entity.serial) ++
         classes.iterator.map(_.entity.serial) ++
         locales.iterator.map(_.entity.serial) ++
         locale_dependencies.iterator.map(_.entity.serial)
@@ -97,7 +97,7 @@
         types.map(_.cache(cache)),
         consts.map(_.cache(cache)),
         axioms.map(_.cache(cache)),
-        facts.map(_.cache(cache)),
+        thms.map(_.cache(cache)),
         classes.map(_.cache(cache)),
         locales.map(_.cache(cache)),
         locale_dependencies.map(_.cache(cache)),
@@ -113,7 +113,7 @@
     types: Boolean = true,
     consts: Boolean = true,
     axioms: Boolean = true,
-    facts: Boolean = true,
+    thms: Boolean = true,
     classes: Boolean = true,
     locales: Boolean = true,
     locale_dependencies: Boolean = true,
@@ -134,7 +134,7 @@
         if (types) read_types(provider) else Nil,
         if (consts) read_consts(provider) else Nil,
         if (axioms) read_axioms(provider) else Nil,
-        if (facts) read_facts(provider) else Nil,
+        if (thms) read_thms(provider) else Nil,
         if (classes) read_classes(provider) else Nil,
         if (locales) read_locales(provider) else Nil,
         if (locale_dependencies) read_locale_dependencies(provider) else Nil,
@@ -166,7 +166,7 @@
     val TYPE = Value("type")
     val CONST = Value("const")
     val AXIOM = Value("axiom")
-    val FACT = Value("fact")
+    val THM = Value("thm")
     val CLASS = Value("class")
     val LOCALE = Value("locale")
     val LOCALE_DEPENDENCY = Value("locale_dependency")
@@ -285,7 +285,7 @@
       })
 
 
-  /* axioms and facts */
+  /* axioms */
 
   sealed case class Prop(
     typargs: List[(String, Term.Sort)],
@@ -310,62 +310,40 @@
     Prop(typargs, args, t)
   }
 
-
-  sealed case class Fact(prop: Prop, proof: Option[Term.Proof])
+  sealed case class Axiom(entity: Entity, prop: Prop)
   {
-    def cache(cache: Term.Cache): Fact =
-      Fact(prop.cache(cache), proof.map(cache.proof _))
-  }
-
-  def decode_fact(body: XML.Body): Fact =
-  {
-    val (prop, proof) =
-    {
-      import XML.Decode._
-      pair(decode_prop _, option(Term_XML.Decode.proof))(body)
-    }
-    Fact(prop, proof)
+    def cache(cache: Term.Cache): Axiom =
+      Axiom(entity.cache(cache), prop.cache(cache))
   }
 
-  sealed case class Fact_Single(entity: Entity, fact: Fact)
-  {
-    def cache(cache: Term.Cache): Fact_Single =
-      Fact_Single(entity.cache(cache), fact.cache(cache))
-
-    def prop: Prop = fact.prop
-    def proof: Option[Term.Proof] = fact.proof
-  }
-
-  sealed case class Fact_Multi(entity: Entity, facts: List[Fact])
-  {
-    def cache(cache: Term.Cache): Fact_Multi =
-      Fact_Multi(entity.cache(cache), facts.map(_.cache(cache)))
-
-    def props: List[Prop] = facts.map(_.prop)
-
-    def split: List[Fact_Single] =
-      facts match {
-        case List(fact) => List(Fact_Single(entity, fact))
-        case _ =>
-          for ((fact, i) <- facts.zipWithIndex)
-          yield Fact_Single(entity.copy(name = entity.name + "(" + (i + 1) + ")"), fact)
-      }
-  }
-
-  def read_axioms(provider: Export.Provider): List[Fact_Single] =
+  def read_axioms(provider: Export.Provider): List[Axiom] =
     provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.AXIOM, tree)
         val prop = decode_prop(body)
-        Fact_Single(entity, Fact(prop, None))
+        Axiom(entity, prop)
       })
 
-  def read_facts(provider: Export.Provider): List[Fact_Multi] =
-    provider.uncompressed_yxml(export_prefix + "facts").map((tree: XML.Tree) =>
+
+  /* theorems */
+
+  sealed case class Thm(entity: Entity, prop: Prop, proof: Option[Term.Proof])
+  {
+    def cache(cache: Term.Cache): Thm =
+      Thm(entity.cache(cache), prop.cache(cache), proof.map(cache.proof _))
+  }
+
+  def read_thms(provider: Export.Provider): List[Thm] =
+    provider.uncompressed_yxml(export_prefix + "thms").map((tree: XML.Tree) =>
       {
-        val (entity, body) = decode_entity(Kind.FACT, tree)
-        val facts = XML.Decode.list(decode_fact)(body)
-        Fact_Multi(entity, facts)
+        val (entity, body) = decode_entity(Kind.THM, tree)
+        val (prop, prf) =
+        {
+          import XML.Decode._
+          import Term_XML.Decode._
+          pair(decode_prop _, option(proof))(body)
+        }
+        Thm(entity, prop, prf)
       })
 
   def read_proof(