src/ZF/Nat_ZF.thy

--- a/src/ZF/Nat_ZF.thy	Thu Mar 15 16:35:02 2012 +0000
+++ b/src/ZF/Nat_ZF.thy	Thu Mar 15 17:38:05 2012 +0000
@@ -92,7 +92,7 @@
 
 lemma natE:
  assumes "n \<in> nat"
- obtains (0) "n=0" | (succ) x where "x \<in> nat" "n=succ(x)"
+ obtains ("0") "n=0" | (succ) x where "x \<in> nat" "n=succ(x)"
 using assms
 by (rule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE]) auto