# HG changeset patch
# User wenzelm
# Date 1184881740 -7200
# Node ID 6c644d14d91d9a1baf504259e7795e869de90feb
# Parent  f449381e2caa5a2c16c745776e1753f511f56e01
added pprint for Path.T, File.ident;

diff -r f449381e2caa -r 6c644d14d91d src/Pure/install_pp.ML
--- a/src/Pure/install_pp.ML	Thu Jul 19 23:18:59 2007 +0200
+++ b/src/Pure/install_pp.ML	Thu Jul 19 23:49:00 2007 +0200
@@ -11,3 +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));