diff -r ee0a0eb6b738 -r 151b3758f576 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sat Sep 29 08:58:51 2007 +0200
+++ b/src/HOL/Lattices.thy	Sat Sep 29 08:58:54 2007 +0200
@@ -401,34 +401,34 @@
   "\<Squnion>{a, b} = a \<squnion> b"
   by (simp add: Sup_insert_simp)
 
-end
-
 definition
-  top :: "'a::complete_lattice"
+  top :: 'a
 where
   "top = Inf {}"
 
 definition
-  bot :: "'a::complete_lattice"
+  bot :: 'a
 where
   "bot = Sup {}"
 
-lemma top_greatest [simp]: "x \<le> top"
+lemma top_greatest [simp]: "x \<^loc>\<le> top"
   by (unfold top_def, rule Inf_greatest, simp)
 
-lemma bot_least [simp]: "bot \<le> x"
+lemma bot_least [simp]: "bot \<^loc>\<le> x"
   by (unfold bot_def, rule Sup_least, simp)
 
 definition
-  SUPR :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b"
+  SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
 where
   "SUPR A f == Sup (f ` A)"
 
 definition
-  INFI :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b"
+  INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
 where
   "INFI A f == Inf (f ` A)"
 
+end
+
 syntax
   "_SUP1"     :: "pttrns => 'b => 'b"           ("(3SUP _./ _)" [0, 10] 10)
   "_SUP"      :: "pttrn => 'a set => 'b => 'b"  ("(3SUP _:_./ _)" [0, 10] 10)