src/FOL/simpdata.ML

--- a/src/FOL/simpdata.ML	Wed Jan 05 19:33:56 1994 +0100
+++ b/src/FOL/simpdata.ML	Wed Jan 05 19:41:37 1994 +0100
@@ -93,7 +93,8 @@
 val IFOL_ss = empty_ss
       setmksimps mk_rew_rules
       setsolver
-        (fn prems => resolve_tac (TrueI::refl::iff_refl::notFalseI::prems))
+        (fn prems => resolve_tac (TrueI::refl::iff_refl::notFalseI::prems)
+                     ORELSE' atac)
       setsubgoaler asm_simp_tac
       addsimps IFOL_rews
       addcongs [imp_cong];