diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/IMP/Expr.thy
--- a/src/HOL/IMP/Expr.thy	Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/IMP/Expr.thy	Mon Sep 11 21:35:19 2006 +0200
@@ -135,10 +135,10 @@
 
 
 lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)"
-  by (induct a fixing: n) auto
+  by (induct a arbitrary: n) auto
 
 lemma bexp_iff:
   "((b,s) -b-> w) = (B b s = w)"
-  by (induct b fixing: w) (auto simp add: aexp_iff)
+  by (induct b arbitrary: w) (auto simp add: aexp_iff)
 
 end