author | wenzelm |
Sun, 07 Jan 2018 12:41:34 +0100 | |
changeset 67355 | 4c8280aaf6ad |
parent 67354 | f243af7b5be3 |
child 67356 | ba226b87c69e |
--- 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 *)