# HG changeset patch
# User wenzelm
# Date 1326398257 -3600
# Node ID d4558296bdc3dff2eb9ce03d0306d370dc023896
# Parent  872f915e3a98d0789a7b6e343359fd827efd457b
tuned;

diff -r 872f915e3a98 -r d4558296bdc3 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Jan 12 20:51:28 2012 +0100
+++ b/src/Pure/Thy/thy_output.ML	Thu Jan 12 20:57:37 2012 +0100
@@ -486,7 +486,7 @@
   if Config.get ctxt display then s else Symbol.strip_blanks s;
 
 fun pretty_text ctxt =
-  Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o Library.split_lines;
+  Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines;
 
 fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;