1.1 --- a/src/HOL/Tools/inductive.ML	Wed May 09 16:46:12 2012 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Thu May 10 20:49:30 2012 +0200
     1.3 @@ -469,7 +469,7 @@
     1.4              fun list_ex ([], t) = t
     1.5                | list_ex ((a, T) :: vars, t) =
     1.6                    HOLogic.exists_const T $ Abs (a, T, list_ex (vars, t));
     1.7 -            val conjs = map2 (curry HOLogic.mk_eq) frees us @ (map HOLogic.dest_Trueprop ts);
     1.8 +            val conjs = map2 (curry HOLogic.mk_eq) frees us @ map HOLogic.dest_Trueprop ts;
     1.9            in
    1.10              list_ex (params', if null conjs then @{term True} else foldr1 HOLogic.mk_conj conjs)
    1.11            end;
    1.12 @@ -479,26 +479,30 @@
    1.13            else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs);
    1.14          val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    1.15          fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
    1.16 -            let
    1.17 -              val (prems', last_prem) = split_last prems;
    1.18 -            in
    1.19 -              EVERY1 (select_disj (length c_intrs) (i + 1)) THEN
    1.20 -              EVERY (replicate (length params) (rtac @{thm exI} 1)) THEN
    1.21 -              EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems') THEN
    1.22 -              rtac last_prem 1
    1.23 -            end) ctxt' 1;
    1.24 +            EVERY1 (select_disj (length c_intrs) (i + 1)) THEN
    1.25 +            EVERY (replicate (length params) (rtac @{thm exI} 1)) THEN
    1.26 +            (if null prems then rtac @{thm TrueI} 1
    1.27 +             else
    1.28 +              let
    1.29 +                val (prems', last_prem) = split_last prems;
    1.30 +              in
    1.31 +                EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems') THEN
    1.32 +                rtac last_prem 1
    1.33 +              end)) ctxt' 1;
    1.34          fun prove_intr2 (((_, _, us, _), ts, params'), intr) =
    1.35            EVERY (replicate (length params') (etac @{thm exE} 1)) THEN
    1.36 -          EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN
    1.37 -          Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
    1.38 -            let
    1.39 -              val (eqs, prems') = chop (length us) prems;
    1.40 -              val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs;
    1.41 -            in
    1.42 -              rewrite_goal_tac rew_thms 1 THEN
    1.43 -              rtac intr 1 THEN
    1.44 -              EVERY (map (fn p => rtac p 1) prems')
    1.45 -            end) ctxt' 1;
    1.46 +          (if null ts andalso null us then rtac intr 1
    1.47 +           else
    1.48 +            EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN
    1.49 +            Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
    1.50 +              let
    1.51 +                val (eqs, prems') = chop (length us) prems;
    1.52 +                val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs;
    1.53 +              in
    1.54 +                rewrite_goal_tac rew_thms 1 THEN
    1.55 +                rtac intr 1 THEN
    1.56 +                EVERY (map (fn p => rtac p 1) prems')
    1.57 +              end) ctxt' 1);
    1.58        in
    1.59          Skip_Proof.prove ctxt' [] [] eq (fn _ =>
    1.60            rtac @{thm iffI} 1 THEN etac (#1 elim) 1 THEN