induct stripped: match_tac;

--- a/src/HOL/Tools/induct_method.ML	Wed Apr 12 18:47:03 2000 +0200
+++ b/src/HOL/Tools/induct_method.ML	Wed Apr 12 18:53:09 2000 +0200
@@ -327,7 +327,7 @@
       Seq.map (rpair cases) (Method.multi_resolves facts [thm]);
     val tac = Method.resolveq_cases_tac (Seq.flat (Seq.map prep_rule (Seq.of_list rules)));
   in
-    if stripped then tac THEN_ALL_NEW_CASES (REPEAT o resolve_tac [impI, allI, ballI])
+    if stripped then tac THEN_ALL_NEW_CASES (REPEAT o Tactic.match_tac [impI, allI, ballI])
     else tac
   end;