# HG changeset patch
# User wenzelm
# Date 1572876956 -3600
# Node ID b697dd74221a35b99cc8f241f412ee57495c6795
# Parent  4003da7e6a7901945aa025f01941df916096ab79
tuned;

diff -r 4003da7e6a79 -r b697dd74221a src/HOL/Proofs/ex/XML_Data.thy
--- a/src/HOL/Proofs/ex/XML_Data.thy	Mon Nov 04 15:14:34 2019 +0100
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Mon Nov 04 15:15:56 2019 +0100
@@ -12,10 +12,9 @@
 subsection \<open>Export and re-import of global proof terms\<close>
 
 ML \<open>
-  fun export_proof thy thm =
-    Proofterm.encode (Sign.consts_of thy)
-      (Proofterm.reconstruct_proof thy (Thm.prop_of thm)
-        (Thm.standard_proof_of {full = true, expand_name = Thm.expand_name thm} thm));
+  fun export_proof thy thm = thm
+    |> Thm.standard_proof_of {full = true, expand_name = Thm.expand_name thm}
+    |> Proofterm.encode (Sign.consts_of thy);
 
   fun import_proof thy xml =
     let