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 \Export and re-import of global proof terms\ ML \ 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