# HG changeset patch
# User wenzelm
# Date 1310494271 -7200
# Node ID c3b6374278fa1793510fd313c3977bae8c3e3c5b
# Parent  ef45eaf2775f6f38d5611bbdd3b23330426a1268
ML pp for XML.tree;

diff -r ef45eaf2775f -r c3b6374278fa src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Tue Jul 12 20:11:00 2011 +0200
+++ b/src/Pure/pure_setup.ML	Tue Jul 12 20:11:11 2011 +0200
@@ -18,6 +18,7 @@
 
 (* ML toplevel pretty printing *)
 
+toplevel_pp ["XML", "tree"] "Pretty.str o XML.string_of";
 toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
 toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
 toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";