unfold min/max in Stefans code generator

--- a/src/HOL/Orderings.thy	Sat May 19 13:41:13 2007 +0200
+++ b/src/HOL/Orderings.thy	Sat May 19 14:05:05 2007 +0200
@@ -91,6 +91,9 @@
   max :: "'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> 'a" where
   "max a b = (if a \<le> b then b else a)"
 
+declare min_def[code unfold, code inline del]
+        max_def[code unfold, code inline del]
+
 lemma linorder_class_min:
   "ord.min (op \<le> \<Colon> 'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> bool) = min"
   by rule+ (simp add: min_def ord_class.min_def)