src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Fri Aug 28 18:52:41 2009 +0200
+++ b/src/HOL/Nat.thy	Fri Aug 28 19:15:59 2009 +0200
@@ -1512,7 +1512,7 @@
 by (simp split add: nat_diff_split)
 
 lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i"
-unfolding min_def by auto
+by auto
 
 lemma inj_on_diff_nat: 
   assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)"