--- a/src/HOL/IMP/Def_Ass_Sound_Big.thy Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Def_Ass_Sound_Big.thy Tue Sep 20 05:48:23 2011 +0200
@@ -12,7 +12,7 @@
theorem Sound:
"\<lbrakk> (c,Some s) \<Rightarrow> s'; D A c A'; A \<subseteq> dom s \<rbrakk>
\<Longrightarrow> \<exists> t. s' = Some t \<and> A' \<subseteq> dom t"
-proof (induct c "Some s" s' arbitrary: s A A' rule:big_step_induct)
+proof (induction c "Some s" s' arbitrary: s A A' rule:big_step_induct)
case AssignNone thus ?case
by auto (metis aval_Some option.simps(3) subset_trans)
next