diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Def_Ass_Sound_Big.thy
--- 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