equal
deleted
inserted
replaced
582 val thy = ProofContext.theory_of ctxt; |
582 val thy = ProofContext.theory_of ctxt; |
583 val prf = Thm.proof_of thm; |
583 val prf = Thm.proof_of thm; |
584 val prop = Thm.full_prop_of thm; |
584 val prop = Thm.full_prop_of thm; |
585 val prf' = Proofterm.rewrite_proof_notypes ([], []) prf |
585 val prf' = Proofterm.rewrite_proof_notypes ([], []) prf |
586 in |
586 in |
587 ProofContext.pretty_proof ctxt |
587 ProofSyntax.pretty_proof ctxt |
588 (if full then Reconstruct.reconstruct_proof thy prop prf' else prf') |
588 (if full then Reconstruct.reconstruct_proof thy prop prf' else prf') |
589 end |
589 end |
590 | SOME args => Pretty.chunks |
590 | SOME args => Pretty.chunks |
591 (map (ProofContext.pretty_proof_of (Proof.context_of state) full) |
591 (map (ProofSyntax.pretty_proof_of (Proof.context_of state) full) |
592 (Proof.get_thmss state args))); |
592 (Proof.get_thmss state args))); |
593 |
593 |
594 fun string_of_prop state s = |
594 fun string_of_prop state s = |
595 let |
595 let |
596 val ctxt = Proof.context_of state; |
596 val ctxt = Proof.context_of state; |