src/HOL/simpdata.ML
changeset 1968 daa97cc96feb
parent 1948 78e5bfcbc1e9
child 1984 5cf82dc3ce67
     1.1 --- a/src/HOL/simpdata.ML	Mon Sep 09 18:58:02 1996 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Tue Sep 10 10:48:07 1996 +0200
     1.3 @@ -16,10 +16,11 @@
     1.4  
     1.5  fun Addss ss = (claset := !claset addbefore asm_full_simp_tac ss 1);
     1.6  
     1.7 -(*Maybe swap the safe_tac and simp_tac lines?**)
     1.8 +(*Designed to be idempotent, except if best_tac instantiates variables
     1.9 +  in some of the subgoals*)
    1.10  fun auto_tac (cs,ss) = 
    1.11 -    TRY (safe_tac cs) THEN 
    1.12      ALLGOALS (asm_full_simp_tac ss) THEN
    1.13 +    REPEAT (safe_tac cs THEN ALLGOALS (asm_full_simp_tac ss)) THEN
    1.14      REPEAT (FIRSTGOAL (best_tac (cs addss ss)));
    1.15  
    1.16  fun Auto_tac() = auto_tac (!claset, !simpset);