src/HOL/datatype.ML

    Author:      Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker,
                 Konrad Slind
    Copyright 1995 TU Muenchen
 *)
 
+(* should go into Pure *)
+fun ALLNEWSUBGOALS tac tacf i =
+  STATE (fn state0 => tac i THEN
+  STATE (fn state1 => let val d = nprems_of state1 - nprems_of state0
+                      in EVERY(map tacf ((i+d) downto i)) end));
 
 (*used for constructor parameters*)
 datatype dt_type = dtVar of string |
   dtTyp of dt_type list * string |
   dtRek of dt_type list * string;

      fun const s = Const(s, the(Sign.const_type sign s))
      val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl
      val {nchotomy,case_cong} = case_thms sign case_rewrites itac
      val exhaustion = mk_exhaust nchotomy
      val exh_var = exhaust_var exhaustion;
-     fun exhaust_tac a = res_inst_tac [(exh_var,a)] exhaustion;
+     fun exhaust_tac a =
+           ALLNEWSUBGOALS (res_inst_tac [(exh_var,a)] exhaustion)
+                          (rotate_tac ~1);
      fun induct_tac a i =
            STATE(fn st =>
              (if Datatype.occs_in_prems a i st
               then warning "Induction variable occurs also among premises!"
               else ();