src/ZF/Induct/PropLog.thy

   -- {* A semantic analogue of the Deduction Theorem *}
   by (simp add: logcon_def)
 
 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)
   apply (blast intro: propn_Is)
   done