# HG changeset patch
# User wenzelm
# Date 1273256206 -7200
# Node ID 5e1f305ae86733a14e804ce5b71d34bb67f6efc6
# Parent  9c2ee10809b2a214c55cd4dec24b7269ee15301f
tuned;

diff -r 9c2ee10809b2 -r 5e1f305ae867 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Fri May 07 19:50:50 2010 +0200
+++ b/src/Pure/General/pretty.ML	Fri May 07 20:16:46 2010 +0200
@@ -145,7 +145,7 @@
 val chunks = markup_chunks Markup.none;
 fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
 
-fun block_enclose (p1, p2) ps = chunks [(block  o fbreaks) (p1 :: ps), p2];
+fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
 
 fun quote prt = blk (1, [str "\"", prt, str "\""]);
 fun backquote prt = blk (1, [str "`", prt, str "`"]);