src/HOL/Library/LaTeXsugar.thy

--- a/src/HOL/Library/LaTeXsugar.thy	Tue Jan 09 15:18:41 2018 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Tue Jan 09 15:40:12 2018 +0100
@@ -104,7 +104,7 @@
             Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
       end
   in
-    Thy_Output.antiquotation @{binding "const_typ"}
+    Document_Antiquotation.setup @{binding "const_typ"}
      (Scan.lift Args.embedded_inner_syntax)
        (fn {source = src, context = ctxt, ...} => fn arg =>
           Thy_Output.output ctxt