diff -r c5d17ae788b2 -r d4bad1efa268 src/Doc/Prog_Prove/Logic.thy
--- a/src/Doc/Prog_Prove/Logic.thy	Fri Aug 24 13:09:35 2018 +0200
+++ b/src/Doc/Prog_Prove/Logic.thy	Fri Aug 24 16:00:41 2018 +0200
@@ -123,7 +123,7 @@
 those of @{text"\<Inter>"} are \texttt{\char`\\\char`\<Inter>} and \texttt{Inter}.
 There are also indexed unions and intersections:
 \begin{center}
-@{thm UNION_eq} \\ @{thm INTER_eq}
+@{thm[eta_contract=false] UNION_eq} \\ @{thm[eta_contract=false] INTER_eq}
 \end{center}
 The ASCII forms are \ \texttt{UN x:A.~B} \ and \ \texttt{INT x:A. B} \
 where \texttt{x} may occur in \texttt{B}.