1.1 --- a/src/HOL/BNF/Tools/coinduction.ML	Tue Nov 05 18:16:16 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/coinduction.ML	Thu Oct 17 17:14:06 2013 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4              map3 (fn name => fn T => fn (_, rhs) =>
     1.5                HOLogic.mk_eq (Free (name, T), rhs))
     1.6              names Ts raw_eqs;
     1.7 -          val phi = map (HOLogic.dest_Trueprop o prop_of) prems @ eqs
     1.8 +          val phi = eqs @ map (HOLogic.dest_Trueprop o prop_of) prems
     1.9              |> try (Library.foldr1 HOLogic.mk_conj)
    1.10              |> the_default @{term True}
    1.11              |> list_exists_free vars
    1.12 @@ -89,8 +89,8 @@
    1.13            HEADGOAL (EVERY' [rtac thm,
    1.14              EVERY' (map (fn var =>
    1.15                rtac (cterm_instantiate_pos [NONE, SOME (certify ctxt var)] exI)) vars),
    1.16 -            EVERY' (map (fn prem => rtac conjI THEN' rtac prem) prems),
    1.17 -            CONJ_WRAP' (K (rtac refl)) eqs,
    1.18 +            if p = 0 then CONJ_WRAP' (K (rtac refl)) eqs
    1.19 +            else REPEAT_DETERM_N e o (rtac conjI THEN' rtac refl) THEN' CONJ_WRAP' rtac prems,
    1.20              K (ALLGOALS_SKIP skip
    1.21                 (REPEAT_DETERM_N (length vars) o (etac exE THEN' rotate_tac ~1) THEN'
    1.22                 DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
    1.23 @@ -100,11 +100,11 @@
    1.24                       let
    1.25                         val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
    1.26                         val inv_thms = init @ [last];
    1.27 -                       val eqs = drop p inv_thms;
    1.28 +                       val eqs = take e inv_thms;
    1.29                         fun is_local_var t = 
    1.30                           member (fn (t, (_, t')) => t aconv (term_of t')) params t;
    1.31                          val (eqs, assms') = filter_in_out (is_local_var o lhs_of_eq o prop_of) eqs;
    1.32 -                        val assms = assms' @ take p inv_thms
    1.33 +                        val assms = assms' @ drop e inv_thms
    1.34                        in
    1.35                          HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN
    1.36                          unfold_thms_tac ctxt eqs