tuned;
authorwenzelm
Thu, 12 Jan 2012 20:57:37 +0100
changeset 46195 d4558296bdc3
parent 46194 872f915e3a98
child 46196 805de058722b
tuned;
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;