# HG changeset patch
# User wenzelm
# Date 1184882500 -7200
# Node ID 307f75aaefcaa0a711de935b8af0fadfcbf2dcab
# Parent  d3b05e7bc5d25af01e346519ad4f5cbe9264758e
tuned;

diff -r d3b05e7bc5d2 -r 307f75aaefca src/Pure/install_pp.ML
--- a/src/Pure/install_pp.ML	Thu Jul 19 23:49:05 2007 +0200
+++ b/src/Pure/install_pp.ML	Fri Jul 20 00:01:40 2007 +0200
@@ -11,5 +11,5 @@
 install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context);
 install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
 install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy));
-install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.quote o Pretty.str o Path.implode));
-install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o File.rep_ident));
+install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.str o quote o Path.implode));
+install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o quote o File.rep_ident));