diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Sem_Equiv.thy
--- a/src/HOL/IMP/Sem_Equiv.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Sem_Equiv.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -83,10 +83,9 @@
          P s \<Longrightarrow> 
          d = WHILE b DO c \<Longrightarrow> 
          (WHILE b' DO c', s) \<Rightarrow> s'"  
-proof (induct rule: big_step_induct)
+proof (induction rule: big_step_induct)
   case (WhileTrue b s1 c s2 s3)
-  note IH = WhileTrue.hyps(5) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
-  
+  note IH = WhileTrue.IH(2) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
   from WhileTrue.prems
   have "P \<Turnstile> b <\<sim>> b'" by simp
   with `bval b s1` `P s1`