# HG changeset patch # User nipkow # Date 887031659 -3600 # Node ID 26764de50c749616b392ed190fe8bc4a0b671ebc # Parent 18a3f33f2097b19e52710d1b300c50ee704b8bb2 Used THEN_ALL_NEW. diff -r 18a3f33f2097 -r 26764de50c74 src/Provers/simplifier.ML --- a/src/Provers/simplifier.ML Sat Feb 07 14:40:05 1998 +0100 +++ b/src/Provers/simplifier.ML Mon Feb 09 14:40:59 1998 +0100 @@ -278,15 +278,11 @@ (** simplification tactics **) -fun NEWSUBGOALS tac tacf st0 = - st0 |> (tac THEN (fn st1 => tacf (nprems_of st1 - nprems_of st0) st1)); - fun solve_all_tac (subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac) mss = let val ss = make_ss (mss, subgoal_tac, loop_tac, unsafe_finish_tac, unsafe_finish_tac); - val solve1_tac = - NEWSUBGOALS (subgoal_tac ss 1) (fn n => if n < 0 then all_tac else no_tac); + val solve1_tac = (subgoal_tac ss THEN_ALL_NEW (K no_tac)) 1 in DEPTH_SOLVE solve1_tac end; @@ -294,13 +290,13 @@ fun basic_gen_simp_tac mode = fn (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac}) => let - fun simp_loop_tac i thm = - (asm_rewrite_goal_tac mode - (solve_all_tac (subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac)) mss i - THEN (finish_tac (prems_of_mss mss) i ORELSE looper i)) thm - and allsimp i n = EVERY (map (fn j => simp_loop_tac (i + j)) (n downto 0)) - and looper i = TRY (NEWSUBGOALS (loop_tac i) (allsimp i)); - in simp_loop_tac end; + fun simp_loop_tac i = + asm_rewrite_goal_tac mode + (solve_all_tac (subgoal_tac,loop_tac,finish_tac,unsafe_finish_tac)) + mss i + THEN (finish_tac (prems_of_mss mss) i ORELSE + TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i)) + in simp_loop_tac end; fun gen_simp_tac mode (ss as Simpset {unsafe_finish_tac, ...}) = basic_gen_simp_tac mode (ss setSSolver unsafe_finish_tac);