equal
deleted
inserted
replaced
330 |
330 |
331 val prop_of' = Envir.beta_eta_contract oo prop_of0; |
331 val prop_of' = Envir.beta_eta_contract oo prop_of0; |
332 val prop_of = prop_of' []; |
332 val prop_of = prop_of' []; |
333 |
333 |
334 fun proof_of ctxt raw_thm = |
334 fun proof_of ctxt raw_thm = |
335 let val thm = Thm.transfer (Proof_Context.theory_of ctxt) raw_thm |
335 let val thm = Thm.transfer' ctxt raw_thm |
336 in reconstruct_proof ctxt (Thm.prop_of thm) (Thm.proof_of thm) end; |
336 in reconstruct_proof ctxt (Thm.prop_of thm) (Thm.proof_of thm) end; |
337 |
337 |
338 |
338 |
339 |
339 |
340 (**** expand and reconstruct subproofs ****) |
340 (**** expand and reconstruct subproofs ****) |