doc-src/Main/Docs/Main_Doc.thy

       (Args.term -- Args.typ_abbrev)
       (fn {source, context = ctxt, ...} => fn arg =>
         Thy_Output.output ctxt
           (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg]))
   end
+*}
+setup {*
+  Thy_Output.antiquotation @{binding expanded_typ} (Args.typ >> single)
+    (fn {source, context, ...} => Thy_Output.output context o
+      Thy_Output.maybe_pretty_source Syntax.pretty_typ context source)
 *}
 (*>*)
 text{*
 
 \begin{abstract}

 @{term"converse r"} & @{term[source]"converse r"} & (\verb$^-1$)
 \end{tabular}
 \medskip
 
 \noindent
-Type synonym @{typ"'a rel"} @{text"="} @{typ "('a * 'a)set"}
+Type synonym \ @{typ"'a rel"} @{text"="} @{expanded_typ "'a rel"}
 
 \section{Equiv\_Relations}
 
 \begin{supertabular}{@ {} l @ {~::~} l @ {}}
 @{const Equiv_Relations.equiv} & @{term_type_only Equiv_Relations.equiv "'a set \<Rightarrow> ('a*'a)set\<Rightarrow>bool"}\\