diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Compiler.thy	Sat Apr 28 07:38:22 2012 +0200
@@ -259,13 +259,13 @@
   case (Assign x a s)
   show ?case by (fastforce simp:fun_upd_def cong: if_cong)
 next
-  case (Semi c1 s1 s2 c2 s3)
+  case (Seq c1 s1 s2 c2 s3)
   let ?cc1 = "ccomp c1"  let ?cc2 = "ccomp c2"
   have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cc1,s2,stk)"
-    using Semi.IH(1) by fastforce
+    using Seq.IH(1) by fastforce
   moreover
   have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)"
-    using Semi.IH(2) by fastforce
+    using Seq.IH(2) by fastforce
   ultimately show ?case by simp (blast intro: exec_trans)
 next
   case (WhileTrue b s1 c s2 s3)