# HG changeset patch
# User wenzelm
# Date 1571141650 -7200
# Node ID 80f3a290b35cdb1cd9ad1538ea5813a03c66c3ef
# Parent  de2e2382bc0d930f21368bbf84bba72278a3192c
clarified proof export;

diff -r de2e2382bc0d -r 80f3a290b35c src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Tue Oct 15 13:34:50 2019 +0200
+++ b/src/Pure/Thy/export_theory.scala	Tue Oct 15 14:14:10 2019 +0200
@@ -349,29 +349,41 @@
         Thm(entity, prop, deps, prf)
       })
 
+  sealed case class Proof(
+    typargs: List[(String, Term.Sort)],
+    args: List[(String, Term.Typ)],
+    term: Term.Term,
+    proof: Term.Proof)
+  {
+    def cache(cache: Term.Cache): Proof =
+      Proof(
+        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
+        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
+        cache.term(term),
+        cache.proof(proof))
+  }
+
   def read_proof(
     provider: Export.Provider,
     theory_name: String,
     serial: Long,
-    cache: Option[Term.Cache] = None): (Term.Term, Term.Proof) =
+    cache: Option[Term.Cache] = None): Proof =
   {
     val body = provider.focus(theory_name).uncompressed_yxml(export_prefix_proofs + serial)
     if (body.isEmpty) error("Bad proof export " + serial)
 
-    val (vars, prop_body, proof_body) =
+    val (typargs, (args, (prop_body, proof_body))) =
     {
       import XML.Decode._
       import Term_XML.Decode._
-      triple(list(pair(string, typ)), x => x, x => x)(body)
+      pair(list(pair(string, sort)), pair(list(pair(string, typ)), pair(x => x, x => x)))(body)
     }
-    val env = vars.toMap
+    val env = args.toMap
     val prop = Term_XML.Decode.term_env(env)(prop_body)
     val proof = Term_XML.Decode.proof_env(env)(proof_body)
 
-    cache match {
-      case None => (prop, proof)
-      case Some(cache) => (cache.term(prop), cache.proof(proof))
-    }
+    val result = Proof(typargs, args, prop, proof)
+    cache.map(result.cache(_)) getOrElse result
   }
 
 
diff -r de2e2382bc0d -r 80f3a290b35c src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Oct 15 13:34:50 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Oct 15 14:14:10 2019 +0200
@@ -2125,22 +2125,23 @@
     #> fold_rev (implies_intr_proof o snd) (#constraints ucontext)
   end;
 
-fun encode_export consts =
-  let
-    open XML.Encode Term_XML.Encode;
-    val encode_vars = list (pair string typ);
-    val encode_term = encode_standard_term consts;
-    val encode_proof = encode_standard_proof consts;
-  in triple encode_vars encode_term encode_proof end;
-
 fun export_proof thy i prop prf0 =
   let
     val prf = prf0
       |> reconstruct_proof thy prop
       |> apply_preproc thy;
     val (prop', SOME prf') = (prop, SOME prf) |> standard_vars Name.context;
-    val vars = [] |> add_standard_vars_term prop' |> add_standard_vars prf' |> rev;
-    val xml = encode_export (Sign.consts_of thy) (vars, prop', prf');
+    val args = [] |> add_standard_vars_term prop' |> add_standard_vars prf' |> rev;
+    val typargs = [] |> Term.add_tfrees prop' |> fold_proof_terms Term.add_tfrees prf' |> rev;
+
+    val consts = Sign.consts_of thy;
+    val xml = (typargs, (args, (prop', prf'))) |>
+      let
+        open XML.Encode Term_XML.Encode;
+        val encode_vars = list (pair string typ);
+        val encode_term = encode_standard_term consts;
+        val encode_proof = encode_standard_proof consts;
+      in pair (list (pair string sort)) (pair encode_vars (pair encode_term encode_proof)) end;
     val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
   in
     chunks |> Export.export_params