# HG changeset patch
# User nipkow
# Date 757795634 -3600
# Node ID c972c57e7762a2d183ad033ff73d8110fffdaae8
# Parent  4a10bc05210a72f8903c3381f774df7ba3a075d4
got rid of METAHYPS due to the change of the basic simplification routines
(see update of Pure/{thm,drule,tactic}.ML)

diff -r 4a10bc05210a -r c972c57e7762 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Wed Jan 05 19:43:46 1994 +0100
+++ b/src/Provers/simplifier.ML	Wed Jan 05 19:47:14 1994 +0100
@@ -127,18 +127,12 @@
 
 fun rep_ss(SS{simps,congs,...}) = {simps=simps,congs=congs};
 
-fun add_asms (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) prems =
-  let val rews = flat(map (mk_rews_of_mss mss) prems)
-  in SS{mss= add_prems(add_simps(mss,rews),prems), simps=simps, congs=congs,
-        subgoal_tac=subgoal_tac,finish_tac=finish_tac,
-        loop_tac=loop_tac}
-  end;
-
 fun NEWSUBGOALS tac tacf =
   STATE(fn state0 =>
     tac THEN STATE(fn state1 => tacf(nprems_of state1 - nprems_of state0)));
 
-fun asm_full_simp_tac(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) =
+fun gen_simp_tac mode =
+  fn (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) =>
   let fun solve_all_tac mss =
         let val ss = SS{mss=mss,simps=simps,congs=congs,
                         subgoal_tac=subgoal_tac,
@@ -149,18 +143,17 @@
         in DEPTH_SOLVE(solve1_tac) end
 
       fun simp_loop i thm =
-        tapply(asm_rewrite_goal_tac solve_all_tac mss i THEN
+        tapply(asm_rewrite_goal_tac mode solve_all_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))
       and simp_loop_tac i = Tactic(simp_loop i)
 
-  in fn i => COND (has_fewer_prems 1) no_tac (simp_loop_tac i) end;
+  in simp_loop_tac end;
 
-fun asm_simp_tac ss =
-      METAHYPS(fn prems => asm_full_simp_tac (add_asms ss prems) 1);
-
-fun simp_tac ss = METAHYPS(fn _ => asm_full_simp_tac ss 1);
+val asm_full_simp_tac = gen_simp_tac (true,true);
+val asm_simp_tac = gen_simp_tac (false,true);
+val simp_tac = gen_simp_tac (false,false);
 
 end;