--- a/src/HOL/FunDef.thy Wed Mar 11 10:58:18 2009 +0100
+++ b/src/HOL/FunDef.thy Wed Mar 11 15:56:49 2009 +0100
@@ -229,7 +229,7 @@
definition "max_strict = max_ext pair_less"
definition [code del]: "max_weak = max_ext pair_leq \<union> {({}, {})}"
definition [code del]: "min_strict = min_ext pair_less"
-definition "min_weak = min_ext pair_leq \<union> {({}, {})}"
+definition [code del]: "min_weak = min_ext pair_leq \<union> {({}, {})}"
lemma wf_pair_less[simp]: "wf pair_less"
by (auto simp: pair_less_def)