--- a/src/HOL/FunDef.thy Mon Jul 12 08:58:27 2010 +0200
+++ b/src/HOL/FunDef.thy Mon Jul 12 10:48:37 2010 +0200
@@ -224,11 +224,11 @@
subsection {* Concrete orders for SCNP termination proofs *}
definition "pair_less = less_than <*lex*> less_than"
-definition [code del]: "pair_leq = pair_less^="
+definition "pair_leq = pair_less^="
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 [code del]: "min_weak = min_ext pair_leq \<union> {({}, {})}"
+definition "max_weak = max_ext pair_leq \<union> {({}, {})}"
+definition "min_strict = min_ext pair_less"
+definition "min_weak = min_ext pair_leq \<union> {({}, {})}"
lemma wf_pair_less[simp]: "wf pair_less"
by (auto simp: pair_less_def)