# HG changeset patch
# User wenzelm
# Date 1515418121 -3600
# Node ID 5a049cf984380946650a6c90c93d4c7421f7d2ad
# Parent  17f9fa98ababce4056b952a682b3f2d4f3fc34db
clarified output (see also 909dcdec2122, 34d1913f0b20);

diff -r 17f9fa98abab -r 5a049cf98438 lib/texinputs/isabelle.sty
--- 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
diff -r 17f9fa98abab -r 5a049cf98438 src/Pure/Thy/thy_output.ML
--- 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));