| changeset 67649 | 1e1782c1aedf |
| parent 64986 | b81a048960a3 |
| child 69575 | f77cc54f6d47 |
--- a/src/Pure/Proof/reconstruct.ML Sat Feb 17 20:03:37 2018 +0100 +++ b/src/Pure/Proof/reconstruct.ML Sun Feb 18 15:05:21 2018 +0100 @@ -332,7 +332,7 @@ val prop_of = prop_of' []; fun proof_of ctxt raw_thm = - let val thm = Thm.transfer (Proof_Context.theory_of ctxt) raw_thm + let val thm = Thm.transfer' ctxt raw_thm in reconstruct_proof ctxt (Thm.prop_of thm) (Thm.proof_of thm) end;