diff -r 547460dc5c1e -r 629a4c5e953e src/Doc/Prog_Prove/LaTeXsugar.thy
--- a/src/Doc/Prog_Prove/LaTeXsugar.thy	Mon May 23 20:45:10 2016 +0200
+++ b/src/Doc/Prog_Prove/LaTeXsugar.thy	Mon May 23 21:30:30 2016 +0200
@@ -52,7 +52,7 @@
       end
   in
     Thy_Output.antiquotation @{binding "const_typ"}
-     (Scan.lift Args.name_inner_syntax)
+     (Scan.lift Args.embedded_inner_syntax)
        (fn {source = src, context = ctxt, ...} => fn arg =>
           Thy_Output.output ctxt
             (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))