# HG changeset patch
# User wenzelm
# Date 1218129698 -7200
# Node ID 644e03cb568d9c36b859a513de1c02051c43f0e8
# Parent  a9d16f8b997a29978f2a3bc152a78cca776a0ef3
install_pp Position.T;

diff -r a9d16f8b997a -r 644e03cb568d src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Thu Aug 07 19:21:37 2008 +0200
+++ b/src/Pure/pure_setup.ML	Thu Aug 07 19:21:38 2008 +0200
@@ -28,6 +28,8 @@
 
 (* ML toplevel pretty printing *)
 
+install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.enum "," "{" "}" o
+  map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of));
 install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
 install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
 install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);