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