diff -r f243af7b5be3 -r 4c8280aaf6ad src/Pure/Thy/latex.ML --- 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 *)