diff -r 310114bec0d7 -r ceb324e34c14 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Thu Jan 25 11:29:52 2018 +0100
+++ b/src/Doc/Main/Main_Doc.thy	Thu Jan 25 14:13:55 2018 +0100
@@ -8,11 +8,11 @@
     (fn ctxt => fn (t, T) =>
       (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then ()
        else error "term_type_only: type mismatch";
-       [Syntax.pretty_typ ctxt T]))
+       Syntax.pretty_typ ctxt T))
 \<close>
 setup \<open>
   Thy_Output.antiquotation_pretty_source @{binding expanded_typ} Args.typ
-    (fn ctxt => fn T => [Syntax.pretty_typ ctxt T])
+    Syntax.pretty_typ
 \<close>
 (*>*)
 text\<open>