src/Provers/induct_method.ML

--- a/src/Provers/induct_method.ML	Tue Jan 10 19:33:29 2006 +0100
+++ b/src/Provers/induct_method.ML	Tue Jan 10 19:33:30 2006 +0100
@@ -320,8 +320,7 @@
     (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