changeset 46195 | d4558296bdc3 |
parent 45666 | d83797ef0d2d |
child 46261 | b03897da3c90 |
--- 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;