src/FOL/simpdata.ML
changeset 3206 a3de7f32728c
parent 2801 56948cb1a1f9
child 3537 79ac9b475621
     1.1 --- a/src/FOL/simpdata.ML	Thu May 15 15:47:19 1997 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Thu May 15 15:51:09 1997 +0200
     1.3 @@ -279,23 +279,14 @@
     1.4  			premises to all the premises *)
     1.5  
     1.6  (*Add a simpset to a classical set!*)
     1.7 -infix 4 addss;
     1.8 -fun cs addss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss));
     1.9 -
    1.10 -(*old version, for compatibility with unstable old proofs*)
    1.11 -infix 4 unsafe_addss;
    1.12 -fun cs unsafe_addss ss = cs addbefore asm_full_simp_tac ss;
    1.13 +infix 4 addSss addss;
    1.14 +fun cs addSss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss));
    1.15 +fun cs addss  ss = cs addbefore                        asm_full_simp_tac ss;
    1.16  
    1.17  fun Addss ss = (claset := !claset addss ss);
    1.18  
    1.19  (*Designed to be idempotent, except if best_tac instantiates variables
    1.20    in some of the subgoals*)
    1.21 -(*old version, for compatibility with unstable old proofs*)
    1.22 -fun unsafe_auto_tac (cs,ss) = 
    1.23 -    ALLGOALS (asm_full_simp_tac ss) THEN
    1.24 -    REPEAT (safe_tac cs THEN ALLGOALS (asm_full_simp_tac ss)) THEN
    1.25 -    REPEAT (FIRSTGOAL (best_tac (cs addss ss))) THEN
    1.26 -    prune_params_tac;
    1.27  
    1.28  type clasimpset = (claset * simpset);
    1.29  
    1.30 @@ -317,10 +308,13 @@
    1.31  fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
    1.32  fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
    1.33  
    1.34 -fun auto_tac (cs,ss) = let val cs' = cs addss ss in
    1.35 -EVERY [	TRY (safe_tac cs'),
    1.36 -	REPEAT (FIRSTGOAL (fast_tac cs')),
    1.37 -	prune_params_tac] end;
    1.38 +fun auto_tac (cs,ss) = 
    1.39 +    let val cs' = cs addss ss 
    1.40 +    in  EVERY [TRY (safe_tac cs'),
    1.41 +	       REPEAT (FIRSTGOAL (fast_tac cs')),
    1.42 +               TRY (safe_tac (cs addSss ss)),
    1.43 +	       prune_params_tac] 
    1.44 +    end;
    1.45  
    1.46  fun Auto_tac () = auto_tac (!claset, !simpset);
    1.47