# HG changeset patch
# User wenzelm
# Date 1136918010 -3600
# Node ID ca56111fe69cc64d8d532dc7acab466f757a400b
# Parent  69fe387b3b6e4045bc46428bfc8633bc06674985
fix_tac: no warning;

diff -r 69fe387b3b6e -r ca56111fe69c 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