diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Mon Sep 11 21:35:19 2006 +0200
@@ -2661,7 +2661,7 @@
         \<Longrightarrow> ?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned s0 s1)"
   from eval and wt da G
   show ?thesis
-  proof (induct fixing: Env T A)
+  proof (induct arbitrary: Env T A)
     case (Abrupt s t xc Env T A)
     have da: "Env\<turnstile> dom (locals s) \<guillemotright>t\<guillemotright> A" using Abrupt.prems by simp 
     have "?NormalAssigned (Some xc,s) A"