# HG changeset patch
# User wenzelm
# Date 974036776 -3600
# Node ID acfdc430f4cd9ef9b2d3c30cd06bc5b036df04d8
# Parent  9ef2f60ebde542cb183f7f1a3b931e1f812c3063
removed warning for "stripped" option;

diff -r 9ef2f60ebde5 -r acfdc430f4cd src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Sun Nov 12 14:36:10 2000 +0100
+++ b/src/HOL/Tools/induct_method.ML	Sun Nov 12 14:46:16 2000 +0100
@@ -206,6 +206,8 @@
 fun rulify_cases cert =
   map (apsnd (apsnd (map (Thm.term_of o rulify_cterm o cert)))) ooo RuleCases.make;
 
+val weak_strip_tac = REPEAT o Tactic.match_tac [impI, allI, ballI];
+
 
 infix 1 THEN_ALL_NEW_CASES;
 
@@ -278,10 +280,8 @@
     val tac = Method.resolveq_cases_tac (rulify_cases cert open_parms)
       (Seq.flat (Seq.map prep_rule (Seq.of_list rules)));
   in
-    if stripped then
-      (warning "induct method: encountered deprecated 'stripped' option";
-        tac THEN_ALL_NEW_CASES (REPEAT o Tactic.match_tac [impI, allI, ballI]))
-    else (fn i => Seq.THEN (atomize_tac i, tac i)) THEN_ALL_NEW_CASES rulify_tac
+    (fn i => Seq.THEN (atomize_tac i, tac i)) THEN_ALL_NEW_CASES
+      (rulify_tac THEN' (if stripped then weak_strip_tac else K all_tac))
   end;
 
 in