# HG changeset patch
# User nipkow
# Date 1332950243 -7200
# Node ID e9a3dd1c4cf9b6ac1813e0e6459a5d0dea7f3084
# Parent  da9a2d9e1143099a725f9f20a6988213b2242954
improved robustness with new antiquoation by Makarius

diff -r da9a2d9e1143 -r e9a3dd1c4cf9 doc-src/Main/Docs/Main_Doc.thy
--- a/doc-src/Main/Docs/Main_Doc.thy	Wed Mar 28 16:12:17 2012 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy	Wed Mar 28 17:57:23 2012 +0200
@@ -17,6 +17,11 @@
           (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{*
 
@@ -264,7 +269,7 @@
 \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}
 
diff -r da9a2d9e1143 -r e9a3dd1c4cf9 doc-src/Main/Docs/document/Main_Doc.tex
--- a/doc-src/Main/Docs/document/Main_Doc.tex	Wed Mar 28 16:12:17 2012 +0200
+++ b/doc-src/Main/Docs/document/Main_Doc.tex	Wed Mar 28 17:57:23 2012 +0200
@@ -272,7 +272,7 @@
 \medskip
 
 \noindent
-Type synonym \isa{{\isaliteral{27}{\isacharprime}}a\ rel} \isa{{\isaliteral{3D}{\isacharequal}}} \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}
+Type synonym \ \isa{{\isaliteral{27}{\isacharprime}}a\ rel} \isa{{\isaliteral{3D}{\isacharequal}}} \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}
 
 \section{Equiv\_Relations}