diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/HoareParallel/RG_Hoare.thy
--- a/src/HOL/HoareParallel/RG_Hoare.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -528,7 +528,7 @@
 
 lemma last_length2 [rule_format]: "xs\<noteq>[] \<longrightarrow> (last xs)=(xs!(length xs - (Suc 0)))"
 apply(induct xs,simp+)
-apply(case_tac "length list",simp+)
+apply(case_tac "length xs",simp+)
 done
 
 lemma last_drop: "Suc m<length x \<Longrightarrow> last(drop (Suc m) x) = last x"