| changeset 70443 | a21a96eda033 |
| parent 70418 | d23cfb85438a |
| child 70447 | 755d58b48cec |
--- a/src/Pure/Proof/proof_syntax.ML Tue Jul 30 11:12:52 2019 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Tue Jul 30 11:41:39 2019 +0200 @@ -195,6 +195,6 @@ (Proofterm.term_of_proof prf); fun pretty_clean_proof_of ctxt full thm = - pretty_proof ctxt (Reconstruct.clean_proof_of ctxt full thm); + pretty_proof ctxt (Thm.clean_proof_of ctxt full thm); end;