diff -r 77580c977e0c -r 4b45d592ce29 src/HOL/Proofs/ex/XML_Data.thy
--- a/src/HOL/Proofs/ex/XML_Data.thy	Fri Nov 08 16:25:18 2019 +0100
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Fri Nov 08 19:06:50 2019 +0100
@@ -13,7 +13,7 @@
 
 ML \<open>
   fun export_proof thy thm = thm
-    |> Thm.standard_proof_of {full = true, expand_name = Thm.expand_name thm}
+    |> Proof_Syntax.standard_proof_of {full = true, expand_name = Thm.expand_name thm}
     |> Proofterm.encode (Sign.consts_of thy);
 
   fun import_proof thy xml =