diff -r 6410166400ea -r a21a96eda033 src/HOL/Proofs/ex/XML_Data.thy
--- a/src/HOL/Proofs/ex/XML_Data.thy	Tue Jul 30 11:12:52 2019 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Tue Jul 30 11:41:39 2019 +0200
@@ -13,7 +13,7 @@
 
 ML \<open>
   fun export_proof ctxt thm =
-    Proofterm.encode (Reconstruct.clean_proof_of ctxt true thm);
+    Proofterm.encode (Thm.clean_proof_of ctxt true thm);
 
   fun import_proof thy xml =
     let