Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Proofs/ex/XML_Data.thy
changeset 71088 4b45d592ce29
parent 71021 b697dd74221a
child 71156 1299c8c91ed5 
--- 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 =
isabelle