hide const linorder.less_eq_less.max linorder.less_eq_less.min;

--- a/src/HOL/Orderings.thy	Sun Dec 10 15:30:33 2006 +0100
+++ b/src/HOL/Orderings.thy	Sun Dec 10 15:30:34 2006 +0100
@@ -868,6 +868,8 @@
   max :: "['a::ord, 'a] => 'a"
   "max a b == (if a <= b then b else a)"
 
+hide const linorder.less_eq_less.max linorder.less_eq_less.min  (* FIXME !? *)
+
 lemma min_linorder:
   "linorder.min (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = min"
   by (rule+) (simp add: min_def linorder.min_def)