--- 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 *)