src/HOL/Tools/induct_method.ML
changeset 8688 63b267d41b96
parent 8671 6ce91a80f616
child 8695 850e84526745
equal deleted inserted replaced
8687:24bff69370f0 8688:63b267d41b96
   325 
   325 
   326     fun prep_rule (thm, cases) =
   326     fun prep_rule (thm, cases) =
   327       Seq.map (rpair cases) (Method.multi_resolves facts [thm]);
   327       Seq.map (rpair cases) (Method.multi_resolves facts [thm]);
   328     val tac = Method.resolveq_cases_tac (Seq.flat (Seq.map prep_rule (Seq.of_list rules)));
   328     val tac = Method.resolveq_cases_tac (Seq.flat (Seq.map prep_rule (Seq.of_list rules)));
   329   in
   329   in
   330     if stripped then tac THEN_ALL_NEW_CASES (REPEAT o resolve_tac [impI, allI, ballI])
   330     if stripped then tac THEN_ALL_NEW_CASES (REPEAT o Tactic.match_tac [impI, allI, ballI])
   331     else tac
   331     else tac
   332   end;
   332   end;
   333 
   333 
   334 in
   334 in
   335 
   335