moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;

--- a/src/Pure/Isar/isar_cmd.ML	Wed Jun 18 18:55:05 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Jun 18 18:55:06 2008 +0200
@@ -584,11 +584,11 @@
           val prop = Thm.full_prop_of thm;
           val prf' = Proofterm.rewrite_proof_notypes ([], []) prf
         in
-          ProofContext.pretty_proof ctxt
+          ProofSyntax.pretty_proof ctxt
             (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
         end
     | SOME args => Pretty.chunks
-        (map (ProofContext.pretty_proof_of (Proof.context_of state) full)
+        (map (ProofSyntax.pretty_proof_of (Proof.context_of state) full)
           (Proof.get_thmss state args)));
 
 fun string_of_prop state s =

--- 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);