--- a/src/HOL/Arith.thy	Thu Aug 17 10:32:44 2000 +0200
+++ b/src/HOL/Arith.thy	Thu Aug 17 10:33:13 2000 +0200
@@ -12,7 +12,7 @@
 (*elimination of `-' on nat*)
 lemma nat_diff_split:
     "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))"
-  by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [RS iffD2])
+  by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
 
 ML {* val nat_diff_split = thm "nat_diff_split" *}