diff -r c38c9039dc13 -r 00d8bf2fce42 src/HOL/Library/Graphs.thy
--- a/src/HOL/Library/Graphs.thy	Sat May 19 07:47:51 2007 +0200
+++ b/src/HOL/Library/Graphs.thy	Sat May 19 08:43:15 2007 +0200
@@ -488,9 +488,9 @@
   shows "has_fpath G (p\<langle>i,j\<rangle>)"
   using l
 proof (induct i rule:inc_induct)
-  case 1 show ?case by (auto simp:sub_path_def intro:has_fpath.intros)
+  case base show ?case by (auto simp:sub_path_def intro:has_fpath.intros)
 next
-  case (2 i)
+  case (step i)
   with ipath upt_rec[of i j]
   show ?case
     by (auto simp:sub_path_def has_ipath_def intro:has_fpath.intros)