# HG changeset patch # User wenzelm # Date 1515325294 -3600 # Node ID 4c8280aaf6ad11976644a2adf2f82cb6b2d07a27 # Parent f243af7b5be35297a281ff9a1e6d16506b428722 tuned; 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 *)