src/Pure/Thy/thy_output.ML
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);