diff -r 87f6e8b93221 -r 424c7b1489df simpdata.ML
--- a/simpdata.ML	Sat Feb 12 14:46:21 1994 +0100
+++ b/simpdata.ML	Tue Feb 15 07:55:22 1994 +0100
@@ -94,7 +94,8 @@
 
 val HOL_ss = empty_ss
       setmksimps mk_rews
-      setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac)
+      setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
+                             ORELSE' etac FalseE)
       setsubgoaler asm_simp_tac
       addsimps ([if_True, if_False, o_apply, conj_assoc] @ simp_thms)
       addcongs [imp_cong];