clarified output (see also 909dcdec2122, 34d1913f0b20);

--- a/lib/texinputs/isabelle.sty	Mon Jan 08 14:26:45 2018 +0100
+++ b/lib/texinputs/isabelle.sty	Mon Jan 08 14:28:41 2018 +0100
@@ -39,7 +39,6 @@
 \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 
-\newcommand{\isaantiqcontrol}[1]{\isatt{{\char`\\}{\char`\<}{\char`\^}#1{\char`\>}}}
 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
 
 \newdimen\isa@parindent\newdimen\isa@parskip

--- a/src/Pure/Thy/thy_output.ML	Mon Jan 08 14:26:45 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Jan 08 14:28:41 2018 +0100
@@ -254,7 +254,7 @@
 val output_symbols_antiq =
   (fn Antiquote.Text syms => output_symbols syms
     | Antiquote.Control {name = (name, _), body, ...} =>
-        Latex.string ("\\isaantiqcontrol{" ^ Latex.output_symbols (Symbol.explode name) ^ "}") ::
+        Latex.string (Latex.output_symbols [Symbol.encode (Symbol.Control name)]) ::
           output_symbols body
     | Antiquote.Antiq {body, ...} =>
         Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body));