--- a/src/HOL/Tools/inductive_package.ML Wed Aug 09 20:43:03 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML Wed Aug 09 20:46:58 2000 +0200
@@ -480,7 +480,7 @@
fun mk_cases_i solved elims ss cprop =
let
val prem = Thm.assume cprop;
- val tac = ALLGOALS (InductMethod.simp_case_tac solved ss) THEN prune_params_tac;
+ val tac = TRYALL (InductMethod.simp_case_tac solved ss) THEN prune_params_tac;
fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
in
(case get_first (try mk_elim) elims of