src/HOL/Library/LaTeXsugar.thy
changeset 67463 a5ca98950a91
parent 67399 eab6ce8368fa
child 67505 ceb324e34c14
--- a/src/HOL/Library/LaTeXsugar.thy	Thu Jan 18 21:29:28 2018 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Thu Jan 18 21:41:30 2018 +0100
@@ -96,20 +96,13 @@
   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
   "_asm" :: "prop \<Rightarrow> asms" ("_")
 
-setup\<open>
-  let
-    fun pretty ctxt c =
-      let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c
-      in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
-            Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
-      end
-  in
-    Document_Antiquotation.setup @{binding "const_typ"}
-     (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]))
-  end;
+setup \<open>
+  Thy_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close> (Scan.lift Args.embedded_inner_syntax)
+    (fn ctxt => fn c =>
+      let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c in
+        [Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
+          Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]]
+      end)
 \<close>
 
 setup\<open>