--- 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);