--- a/src/Pure/Syntax/syntax.ML Mon Mar 31 10:28:08 2014 +0200
+++ b/src/Pure/Syntax/syntax.ML Mon Mar 31 12:35:39 2014 +0200
@@ -575,9 +575,9 @@
in
-fun print_gram syn = Pretty.writeln (Pretty.chunks (pretty_gram syn));
-fun print_trans syn = Pretty.writeln (Pretty.chunks (pretty_trans syn));
-fun print_syntax syn = Pretty.writeln (Pretty.chunks (pretty_gram syn @ pretty_trans syn));
+fun print_gram syn = Pretty.writeln_chunks (pretty_gram syn);
+fun print_trans syn = Pretty.writeln_chunks (pretty_trans syn);
+fun print_syntax syn = Pretty.writeln_chunks (pretty_gram syn @ pretty_trans syn);
end;