# HG changeset patch
# User wenzelm
# Date 1541511053 -3600
# Node ID fc24fe9122585b4f496955dc449afc1151551bfb
# Parent  3e9f812c308c419112362731c7238aa0511b2ea2
tuned;

diff -r 3e9f812c308c -r fc24fe912258 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Mon Nov 05 23:15:58 2018 +0100
+++ b/src/Pure/General/pretty.ML	Tue Nov 06 14:30:53 2018 +0100
@@ -326,10 +326,10 @@
 (*unformatted output*)
 fun unformatted prt =
   let
-    fun fmt (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
-      | fmt (Break (_, wd, _)) = Buffer.add (output_spaces wd)
-      | fmt (Str (s, _)) = Buffer.add s;
-  in fmt prt Buffer.empty end;
+    fun out (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold out prts #> Buffer.add en
+      | out (Break (_, wd, _)) = Buffer.add (output_spaces wd)
+      | out (Str (s, _)) = Buffer.add s;
+  in out prt Buffer.empty end;
 
 
 (* output interfaces *)