src/ZF/Induct/PropLog.thy

--- a/src/ZF/Induct/PropLog.thy	Mon Sep 11 14:35:30 2006 +0200
+++ b/src/ZF/Induct/PropLog.thy	Mon Sep 11 21:35:19 2006 +0200
@@ -327,7 +327,7 @@
 
 lemma completeness:
      "H \<in> Fin(propn) ==> p \<in> propn \<Longrightarrow> H |= p \<Longrightarrow> H |- p"
-  apply (induct fixing: p set: Fin)
+  apply (induct arbitrary: p set: Fin)
    apply (safe intro!: completeness_0)
   apply (rule weaken_left_cons [THEN thms_MP])
    apply (blast intro!: logcon_Imp propn.intros)