| changeset 61865 | 6dcc9e4f1aa6 |
| parent 61814 | 1ca1142e1711 |
| child 61877 | 276ad4354069 |
--- a/src/Pure/Thy/thy_output.ML Sat Dec 19 14:47:52 2015 +0100 +++ b/src/Pure/Thy/thy_output.ML Sat Dec 19 15:14:59 2015 +0100 @@ -602,7 +602,7 @@ fun verbatim_text ctxt = if Config.get ctxt display then - split_lines #> map (prefix (Pretty.spaces (Config.get ctxt indent))) #> cat_lines #> + split_lines #> map (prefix (Symbol.spaces (Config.get ctxt indent))) #> cat_lines #> Latex.output_ascii #> Latex.environment "isabellett" else split_lines #>