miniscoping of nat_diff_split

--- a/src/HOL/NatArith.thy	Tue Dec 05 18:57:40 2000 +0100
+++ b/src/HOL/NatArith.thy	Wed Dec 06 10:23:06 2000 +0100
@@ -11,7 +11,7 @@
 
 (*elimination of `-' on nat*)
 lemma nat_diff_split:
-    "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))"
+    "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
   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" *}