# HG changeset patch
# User wenzelm
# Date 955558389 -7200
# Node ID 63b267d41b96ed9606c7cd45c62edb751b16da0a
# Parent  24bff69370f0dc373c55bf9d67f4a17ac4962cfb
induct stripped: match_tac;

diff -r 24bff69370f0 -r 63b267d41b96 src/HOL/Tools/induct_method.ML
--- 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;