changeset 67355 | 4c8280aaf6ad |
parent 67353 | 95f5f4bec7af |
child 67358 | dfee70a24f0c |
--- a/src/Pure/Thy/latex.ML Sat Jan 06 21:25:16 2018 +0100 +++ b/src/Pure/Thy/latex.ML Sun Jan 07 12:41:34 2018 +0100 @@ -76,7 +76,9 @@ end; -fun enclose_body bg en body = string bg :: body @ [string en]; +fun enclose_body bg en body = + (if bg = "" then [] else [string bg]) @ body @ + (if en = "" then [] else [string en]); (* output name for LaTeX macros *)