src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Sun Jan 18 13:58:17 2009 +0100
+++ b/src/HOL/Nat.thy	Wed Jan 28 16:29:16 2009 +0100
@@ -1254,7 +1254,7 @@
 begin
 
 lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
-  by (simp add: compare_rls of_nat_add [symmetric])
+by (simp add: algebra_simps of_nat_add [symmetric])
 
 end