min_weak_def [code del]

--- 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)

--- a/src/HOL/ex/ExecutableContent.thy	Wed Mar 11 10:58:18 2009 +0100
+++ b/src/HOL/ex/ExecutableContent.thy	Wed Mar 11 15:56:49 2009 +0100
@@ -24,6 +24,4 @@
   "~~/src/HOL/ex/Records"
 begin
 
-declare min_weak_def [code del]
-
 end