src/Provers/simplifier.ML
changeset 1512 ce37c64244c0
parent 1260 c76ac4a9dc2b
child 1676 db29ab9c1490
     1.1 --- a/src/Provers/simplifier.ML	Fri Feb 16 17:24:51 1996 +0100
     1.2 +++ b/src/Provers/simplifier.ML	Fri Feb 16 18:00:47 1996 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4    val Asm_full_simp_tac: int -> tactic
     1.5  end;
     1.6  
     1.7 -functor SimplifierFun():SIMPLIFIER =
     1.8 +structure Simplifier :SIMPLIFIER =
     1.9  struct
    1.10  
    1.11  datatype simpset =
    1.12 @@ -158,14 +158,11 @@
    1.13                            (fn n => if n<0 then all_tac else no_tac)
    1.14          in DEPTH_SOLVE(solve1_tac) end
    1.15  
    1.16 -      fun simp_loop i thm =
    1.17 -        tapply(asm_rewrite_goal_tac mode solve_all_tac mss i THEN
    1.18 -               (finish_tac (prems_of_mss mss) i  ORELSE  looper i),
    1.19 -               thm)
    1.20 +      fun simp_loop_tac i thm =
    1.21 +	  (asm_rewrite_goal_tac mode solve_all_tac mss i THEN
    1.22 +	   (finish_tac (prems_of_mss mss) i  ORELSE  looper i))  thm
    1.23        and allsimp i n = EVERY(map (fn j => simp_loop_tac (i+j)) (n downto 0))
    1.24        and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i))
    1.25 -      and simp_loop_tac i = Tactic(simp_loop i)
    1.26 -
    1.27    in simp_loop_tac end;
    1.28  
    1.29  val asm_full_simp_tac = gen_simp_tac (true,true);