diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/Induct/PropLog.thy
--- a/src/HOL/Induct/PropLog.thy	Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Induct/PropLog.thy	Mon Sep 11 21:35:19 2006 +0200
@@ -259,7 +259,7 @@
 by (unfold sat_def, auto)
 
 theorem completeness: "finite H ==> H |= p ==> H |- p"
-apply (induct fixing: p rule: finite_induct)
+apply (induct arbitrary: p rule: finite_induct)
  apply (blast intro: completeness_0)
 apply (iprover intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP])
 done