src/Pure/Thy/export_theory.scala

         }
         Const(entity, syntax, args, typ, abbrev, propositional, primrec_types, corecursive)
       })
 
 
-  /* facts */
+  /* axioms and facts */
 
   sealed case class Prop(
     typargs: List[(String, Term.Sort)],
     args: List[(String, Term.Typ)],
     term: Term.Term)

       triple(list(pair(string, sort)), list(pair(string, typ)), term)(body)
     }
     Prop(typargs, args, t)
   }
 
-  sealed case class Fact_Single(entity: Entity, prop: Prop)
+
+  sealed case class Fact(prop: Prop, proof: Option[Term.Proof])
+  {
+    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)
+  }
+
+  sealed case class Fact_Single(entity: Entity, fact: Fact)
   {
     def cache(cache: Term.Cache): Fact_Single =
-      Fact_Single(entity.cache(cache), prop.cache(cache))
-  }
-
-  sealed case class Fact_Multi(entity: Entity, props: List[Prop])
+      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), props.map(_.cache(cache)))
+      Fact_Multi(entity.cache(cache), facts.map(_.cache(cache)))
+
+    def props: List[Prop] = facts.map(_.prop)
 
     def split: List[Fact_Single] =
-      props match {
-        case List(prop) => List(Fact_Single(entity, prop))
+      facts match {
+        case List(fact) => List(Fact_Single(entity, fact))
         case _ =>
-          for ((prop, i) <- props.zipWithIndex)
-          yield Fact_Single(entity.copy(name = entity.name + "(" + (i + 1) + ")"), prop)
+          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] =
     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, prop)
+        Fact_Single(entity, Fact(prop, None))
       })
 
   def read_facts(provider: Export.Provider): List[Fact_Multi] =
     provider.uncompressed_yxml(export_prefix + "facts").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.FACT, tree)
-        val props = XML.Decode.list(decode_prop)(body)
-        Fact_Multi(entity, props)
+        val facts = XML.Decode.list(decode_fact)(body)
+        Fact_Multi(entity, facts)
       })
 
 
   /* type classes */