diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/ASM.thy
--- a/src/HOL/IMP/ASM.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/ASM.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -29,7 +29,7 @@
 
 lemma aexec_append[simp]:
   "aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
-apply(induct is1 arbitrary: stk)
+apply(induction is1 arbitrary: stk)
 apply (auto)
 done
 
@@ -44,7 +44,7 @@
 value "acomp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
 
 theorem aexec_acomp[simp]: "aexec (acomp a) s stk = aval a s # stk"
-apply(induct a arbitrary: stk)
+apply(induction a arbitrary: stk)
 apply (auto)
 done