changeset 27258 | 656cfac246be |
parent 26996 | 090a619e7d87 |
child 27344 | d44490b06190 |
--- a/src/Pure/Thy/thy_output.ML Wed Jun 18 18:55:05 2008 +0200 +++ b/src/Pure/Thy/thy_output.ML Wed Jun 18 18:55:06 2008 +0200 @@ -479,7 +479,7 @@ pretty_term_style ctxt (name, Thm.full_prop_of th); fun pretty_prf full ctxt thms = - Pretty.chunks (map (ProofContext.pretty_proof_of ctxt full) thms); + Pretty.chunks (map (ProofSyntax.pretty_proof_of ctxt full) thms); fun pretty_theory ctxt name = (Theory.requires (ProofContext.theory_of ctxt) name "presentation"; Pretty.str name);