tuned

--- a/src/HOL/Nat.thy	Thu Sep 30 07:34:06 2010 +0200
+++ b/src/HOL/Nat.thy	Thu Sep 30 08:50:45 2010 +0200
@@ -149,11 +149,10 @@
 
 primrec minus_nat
 where
-  diff_0:     "m - 0 = (m\<Colon>nat)"
-  | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
+  diff_0 [code]: "m - 0 = (m\<Colon>nat)"
+| diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
 
 declare diff_Suc [simp del]
-declare diff_0 [code]
 
 lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)"
   by (induct n) (simp_all add: diff_Suc)