diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/GCD.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -1558,8 +1558,8 @@
 interpretation gcd_lcm_complete_lattice_nat:
   complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
 where
-  "Inf.INFI Gcd A f = Gcd (f ` A :: nat set)"
-  and "Sup.SUPR Lcm A f = Lcm (f ` A)"
+  "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
+  and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
 proof -
   show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
   proof
@@ -1577,8 +1577,8 @@
   qed
   then interpret gcd_lcm_complete_lattice_nat:
     complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
-  from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFI Gcd A f = Gcd (f ` A)" .
-  from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPR Lcm A f = Lcm (f ` A)" .
+  from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFIMUM Gcd A f = Gcd (f ` A)" .
+  from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPREMUM Lcm A f = Lcm (f ` A)" .
 qed
 
 declare gcd_lcm_complete_lattice_nat.Inf_image_eq [simp del]