--- a/src/HOL/Nat.thy Wed Apr 29 13:36:29 2009 -0700
+++ b/src/HOL/Nat.thy Wed Apr 29 17:15:01 2009 -0700
@@ -1274,10 +1274,10 @@
text{*Special cases where either operand is zero*}
lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
- by (rule of_nat_eq_iff [of 0, simplified])
+ by (rule of_nat_eq_iff [of 0 n, unfolded of_nat_0])
lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
- by (rule of_nat_eq_iff [of _ 0, simplified])
+ by (rule of_nat_eq_iff [of m 0, unfolded of_nat_0])
lemma inj_of_nat: "inj of_nat"
by (simp add: inj_on_def)