# HG changeset patch
# User nipkow
# Date 757795297 -3600
# Node ID bc439e9ce95866ad24ab7795a43de8187a2b79e9
# Parent  ed6a3e2b1a33bffd1b1e9aad4fdd58145cc7f467
updated solver of FOL_ss. see change of HOL/simpdata.ML

diff -r ed6a3e2b1a33 -r bc439e9ce958 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];