# HG changeset patch
# User wenzelm
# Date 1571339039 -7200
# Node ID 8017d382a0d7b7b753afedab727ffdab7f965d7b
# Parent  2a318149b01b789af7c8f5b8385db63e51c042a9
tuned signature;

diff -r 2a318149b01b -r 8017d382a0d7 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Thu Oct 17 20:56:18 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Thu Oct 17 21:03:59 2019 +0200
@@ -271,12 +271,12 @@
           SOME (if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm else MinProof)
           |> standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm);
       in
-        (prop, (deps, (proof, boxes))) |>
+        (prop, (deps, (boxes, proof))) |>
           let
             open XML.Encode Term_XML.Encode;
+            fun encode_box {serial, theory_name} = pair int string (serial, theory_name);
             val encode_proof = Proofterm.encode_standard_proof consts;
-            fun encode_box {serial, theory_name} = pair int string (serial, theory_name);
-          in pair encode_prop (pair (list string) (pair encode_proof (list encode_box))) end
+          in pair encode_prop (pair (list string) (pair (list encode_box) encode_proof)) end
       end;
 
     fun buffer_export_thm (serial, thm_name) =
diff -r 2a318149b01b -r 8017d382a0d7 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Thu Oct 17 20:56:18 2019 +0200
+++ b/src/Pure/Thy/export_theory.scala	Thu Oct 17 21:03:59 2019 +0200
@@ -352,23 +352,23 @@
     entity: Entity,
     prop: Prop,
     deps: List[String],
-    proof: Term.Proof,
-    proof_boxes: List[Thm_Id])
+    proof_boxes: List[Thm_Id],
+    proof: Term.Proof)
   {
     def cache(cache: Term.Cache): Thm =
       Thm(
         entity.cache(cache),
         prop.cache(cache),
         deps.map(cache.string _),
-        cache.proof(proof),
-        proof_boxes.map(_.cache(cache)))
+        proof_boxes.map(_.cache(cache)),
+        cache.proof(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.THM, tree)
-        val (prop, (deps, (prf, prf_boxes))) =
+        val (prop, (deps, (prf_boxes, prf))) =
         {
           import XML.Decode._
           import Term_XML.Decode._
@@ -377,9 +377,9 @@
             val (serial, theory_name) = pair(long, string)(body)
             Thm_Id(serial, theory_name)
           }
-          pair(decode_prop _, pair(list(string), pair(proof, list(thm_id))))(body)
+          pair(decode_prop _, pair(list(string), pair(list(thm_id), proof)))(body)
         }
-        Thm(entity, prop, deps, prf, prf_boxes)
+        Thm(entity, prop, deps, prf_boxes, prf)
       })
 
   sealed case class Proof(