src/HOL/simpdata.ML
changeset 2036 62ff902eeffc
parent 2031 03a843f0f447
child 2054 bf3891343aa5
     1.1 --- a/src/HOL/simpdata.ML	Thu Sep 26 16:12:25 1996 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Thu Sep 26 16:38:02 1996 +0200
     1.3 @@ -23,7 +23,8 @@
     1.4  fun auto_tac (cs,ss) = 
     1.5      ALLGOALS (asm_full_simp_tac ss) THEN
     1.6      REPEAT (safe_tac cs THEN ALLGOALS (asm_full_simp_tac ss)) THEN
     1.7 -    REPEAT (FIRSTGOAL (best_tac (cs addss ss)));
     1.8 +    REPEAT (FIRSTGOAL (best_tac (cs addss ss))) THEN
     1.9 +    prune_params_tac;
    1.10  
    1.11  fun Auto_tac() = auto_tac (!claset, !simpset);
    1.12