# HG changeset patch
# User wenzelm
# Date 1213808106 -7200
# Node ID 656cfac246be6b53685c930c4176e52eeda3cc11
# Parent  ddc00dbad26bf259ef4d2964590d85ed4347475a
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;

diff -r ddc00dbad26b -r 656cfac246be src/Pure/Isar/isar_cmd.ML
--- 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 =
diff -r ddc00dbad26b -r 656cfac246be src/Pure/Thy/thy_output.ML
--- 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);