src/Provers/induct_method.ML

       | goal_concl _ _ _ = NONE;
   in
     (case goal_concl n [] goal of
       SOME concl =>
         (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' rtac asm_rl) i
-    | NONE => (warning ("Induction: no variable " ^ quote (ProofContext.string_of_term ctxt v) ^
-        " to be fixed -- ignored"); all_tac))
+    | NONE => all_tac)
   end);
 
 fun miniscope_tac p i = PRIMITIVE (Drule.fconv_rule
   (Drule.goals_conv (Library.equal i)
     (Drule.forall_conv p (Tactic.rewrite true [Thm.symmetric Drule.norm_hhf_eq]))));