src/HOL/Tools/inductive_package.ML
changeset 9562 6b07b56aa3a8
parent 9405 3235873fdd90
child 9598 65ee72db0236
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Aug 09 20:43:03 2000 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Aug 09 20:46:58 2000 +0200
     1.3 @@ -480,7 +480,7 @@
     1.4  fun mk_cases_i solved elims ss cprop =
     1.5    let
     1.6      val prem = Thm.assume cprop;
     1.7 -    val tac = ALLGOALS (InductMethod.simp_case_tac solved ss) THEN prune_params_tac;
     1.8 +    val tac = TRYALL (InductMethod.simp_case_tac solved ss) THEN prune_params_tac;
     1.9      fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
    1.10    in
    1.11      (case get_first (try mk_elim) elims of