diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/IMP/Machines.thy
--- a/src/HOL/IMP/Machines.thy	Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/IMP/Machines.thy	Mon Sep 11 21:35:19 2006 +0200
@@ -192,7 +192,7 @@
  "rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow>
   rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow>
           rev p' @ q' = rev p @ q \<longrightarrow> \<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>"
-apply(induct fixing: p q p' q' set: exec01)
+apply(induct arbitrary: p q p' q' set: exec01)
    apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
    apply(drule sym)
    apply simp