--- a/src/HOL/Imperative_HOL/ex/Sublist.thy Wed Oct 12 16:21:07 2011 +0200
+++ b/src/HOL/Imperative_HOL/ex/Sublist.thy Wed Oct 12 20:16:48 2011 +0200
@@ -408,7 +408,7 @@
by (induct xs arbitrary: i j, auto)
lemma sublist'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = xs ! i # sublist' (Suc i) j xs"
-apply (induct xs arbitrary: a i j)
+apply (induct xs arbitrary: i j)
apply simp
apply (case_tac j)
apply simp
@@ -418,7 +418,7 @@
done
lemma sublist'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]"
-apply (induct xs arbitrary: a i j)
+apply (induct xs arbitrary: i j)
apply simp
apply simp
done