changeset 55725 | 9d605a21d7ec |
parent 52788 | da1fdbfebd39 |
child 56161 | 300f613060b0 |
--- a/src/Pure/Proof/proof_syntax.ML Mon Feb 24 13:52:48 2014 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Mon Feb 24 14:58:40 2014 +0100 @@ -246,7 +246,7 @@ fun pretty_proof ctxt prf = Proof_Context.pretty_term_abbrev - (Proof_Context.transfer_syntax (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt) + (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt) (term_of_proof prf); fun pretty_proof_of ctxt full th =