--- a/src/HOL/Library/Transitive_Closure_Table.thy Sun Jan 10 18:11:00 2010 +0100
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Sun Jan 10 18:37:37 2010 +0100
@@ -17,11 +17,11 @@
assume "r\<^sup>*\<^sup>* x y"
then show "\<exists>xs. rtrancl_path r x xs y"
proof (induct rule: converse_rtranclp_induct)
- case 1
+ case base
have "rtrancl_path r y [] y" by (rule rtrancl_path.base)
then show ?case ..
next
- case (2 x z)
+ case (step x z)
from `\<exists>xs. rtrancl_path r z xs y`
obtain xs where "rtrancl_path r z xs y" ..
with `r x z` have "rtrancl_path r x (z # xs) y"