
diff -r 69592ac04836 -r b81a048960a3 src/HOL/Proofs/ex/XML_Data.thy
--- a/src/HOL/Proofs/ex/XML_Data.thy	Sat Feb 04 20:12:27 2017 +0100
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Sat Feb 04 21:15:11 2017 +0100
@@ -6,25 +6,14 @@
 *)
 
 theory XML_Data
-imports "~~/src/HOL/Isar_Examples/Drinker"
+  imports "~~/src/HOL/Isar_Examples/Drinker"
 begin
 
 subsection \<open>Export and re-import of global proof terms\<close>
 
 ML \<open>
   fun export_proof ctxt thm =
-    let
-      val thy = Proof_Context.theory_of ctxt;
-      val (_, prop) =
-        Logic.unconstrainT (Thm.shyps_of thm)
-          (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
-      val prf =
-        Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) |>
-        Reconstruct.reconstruct_proof ctxt prop |>
-        Reconstruct.expand_proof ctxt [("", NONE)] |>
-        Proofterm.rew_proof thy |>
-        Proofterm.no_thm_proofs;
-    in Proofterm.encode prf end;
+    Proofterm.encode (Reconstruct.clean_proof_of ctxt true thm);
 
   fun import_proof thy xml =
     let




