diff -r 2b6e55924af3 -r d8b3412cdb99 src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Thu Mar 15 16:35:02 2012 +0000
+++ b/src/ZF/Ordinal.thy	Thu Mar 15 17:38:05 2012 +0000
@@ -703,7 +703,7 @@
 
 lemma Ord_cases:
  assumes i: "Ord(i)"
- obtains (0) "i=0" | (succ) j where "Ord(j)" "i=succ(j)" | (limit) "Limit(i)"
+ obtains ("0") "i=0" | (succ) j where "Ord(j)" "i=succ(j)" | (limit) "Limit(i)"
 by (insert Ord_cases_disj [OF i], auto)
 
 lemma trans_induct3_raw: