diff -r 5e396bcf749e -r 261bd4678076 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Jul 23 22:18:05 2007 +0200
+++ b/src/HOL/Orderings.thy	Tue Jul 24 15:20:45 2007 +0200
@@ -195,14 +195,11 @@
 
 definition (in ord)
   min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
-  "min a b = (if a \<^loc>\<le> b then a else b)"
+  [code unfold, code inline del]: "min a b = (if a \<^loc>\<le> b then a else b)"
 
 definition (in ord)
   max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
-  "max a b = (if a \<^loc>\<le> b then b else a)"
-
-lemmas (in -) min_def [code func, code unfold, code inline del] = min_def [folded ord_class.min]
-lemmas (in -) max_def [code func, code unfold, code inline del] = max_def [folded ord_class.max]
+  [code unfold, code inline del]: "max a b = (if a \<^loc>\<le> b then b else a)"
 
 lemma min_le_iff_disj:
   "min x y \<^loc>\<le> z \<longleftrightarrow> x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
@@ -238,7 +235,8 @@
 
 end
 
-subsection {* Name duplicates -- including min/max interpretation *}
+
+subsection {* Name duplicates *}
 
 lemmas order_less_le = less_le
 lemmas order_eq_refl = order_class.eq_refl
@@ -275,14 +273,14 @@
 lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
 lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
 
-lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [folded ord_class.min]
-lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [folded ord_class.max]
-lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [folded ord_class.min]
-lemmas less_max_iff_disj = linorder_class.less_max_iff_disj [folded ord_class.max]
-lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj [folded ord_class.min]
-lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj [folded ord_class.max]
-lemmas split_min = linorder_class.split_min [folded ord_class.min]
-lemmas split_max = linorder_class.split_max [folded ord_class.max]
+lemmas min_le_iff_disj = linorder_class.min_le_iff_disj
+lemmas le_max_iff_disj = linorder_class.le_max_iff_disj
+lemmas min_less_iff_disj = linorder_class.min_less_iff_disj
+lemmas less_max_iff_disj = linorder_class.less_max_iff_disj
+lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj
+lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj
+lemmas split_min = linorder_class.split_min
+lemmas split_max = linorder_class.split_max
 
 
 subsection {* Reasoning tools setup *}