# HG changeset patch
# User paulson
# Date 842345287 -7200
# Node ID daa97cc96febbd9aa0e1187071906146d4853457
# Parent  0ff58b41c037cf2280b8c325b52d8fb5d71318e6
Beefed-up auto-tactic: now repeatedly simplifies if needed

diff -r 0ff58b41c037 -r daa97cc96feb src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Mon Sep 09 18:58:02 1996 +0200
+++ b/src/HOL/simpdata.ML	Tue Sep 10 10:48:07 1996 +0200
@@ -16,10 +16,11 @@
 
 fun Addss ss = (claset := !claset addbefore asm_full_simp_tac ss 1);
 
-(*Maybe swap the safe_tac and simp_tac lines?**)
+(*Designed to be idempotent, except if best_tac instantiates variables
+  in some of the subgoals*)
 fun auto_tac (cs,ss) = 
-    TRY (safe_tac cs) THEN 
     ALLGOALS (asm_full_simp_tac ss) THEN
+    REPEAT (safe_tac cs THEN ALLGOALS (asm_full_simp_tac ss)) THEN
     REPEAT (FIRSTGOAL (best_tac (cs addss ss)));
 
 fun Auto_tac() = auto_tac (!claset, !simpset);