diff -r dacc380ab327 -r e7df93d4d9b8 src/Doc/Locales/Examples3.thy
--- a/src/Doc/Locales/Examples3.thy	Thu Aug 25 20:08:40 2016 +0200
+++ b/src/Doc/Locales/Examples3.thy	Thu Aug 25 20:08:41 2016 +0200
@@ -91,8 +91,8 @@
 \begin{tabular}{l}
   @{thm [source] int.less_def} from locale @{text partial_order}: \\
   \quad @{thm int.less_def} \\
-  @{thm [source] int.ex_sup} from locale @{text lattice}: \\
-  \quad @{thm int.ex_sup} \\
+  @{thm [source] int.meet_left} from locale @{text lattice}: \\
+  \quad @{thm int.meet_left} \\
   @{thm [source] int.join_distr} from locale @{text distrib_lattice}: \\
   \quad @{thm int.join_distr} \\
   @{thm [source] int.less_total} from locale @{text total_order}: \\