# HG changeset patch
# User nipkow
# Date 887044175 -3600
# Node ID 67a726003cf89df540b6263dc24b316fcd955008
# Parent  26764de50c749616b392ed190fe8bc4a0b671ebc
Replaced ALLNEWSUBGOALS by THEN_ALL_NEW

diff -r 26764de50c74 -r 67a726003cf8 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Feb 09 14:40:59 1998 +0100
+++ b/src/HOL/Nat.thy	Mon Feb 09 18:09:35 1998 +0100
@@ -16,8 +16,8 @@
 ("nat", {case_const = Bound 0, case_rewrites = [],
   constructors = [], induct_tac = nat_ind_tac,
   exhaustion = natE,
-  exhaust_tac = fn v => ALLNEWSUBGOALS (res_inst_tac [("n",v)] natE)
-                                       (rotate_tac ~1),
+  exhaust_tac = fn v => (res_inst_tac [("n",v)] natE)
+                        THEN_ALL_NEW (rotate_tac ~1),
   nchotomy = ProtoPure.flexpair_def, case_cong = ProtoPure.flexpair_def})
 |}
 
diff -r 26764de50c74 -r 67a726003cf8 src/HOL/datatype.ML
--- a/src/HOL/datatype.ML	Mon Feb 09 14:40:59 1998 +0100
+++ b/src/HOL/datatype.ML	Mon Feb 09 18:09:35 1998 +0100
@@ -78,13 +78,6 @@
 end;
 
 
-(* should go into Pure *)
-fun ALLNEWSUBGOALS tac tacf i st0 = st0 |>
-  (tac i THEN
-   (fn st1 => st1 |> 
-        let val d = nprems_of st1 - nprems_of st0
-        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 |
@@ -977,9 +970,8 @@
      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 =
-           ALLNEWSUBGOALS (res_inst_tac [(exh_var,a)] exhaustion)
-                          (rotate_tac ~1);
+     fun exhaust_tac a =  (res_inst_tac [(exh_var,a)] exhaustion)
+                          THEN_ALL_NEW (rotate_tac ~1);
      val induct_tac = Datatype.occs_in_prems itac 
  in
   (ty, {constructors = map(fn s => const s handle _ => const("op "^s)) cl,