FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the
simplifier can rewrite premises, it can generate the premise False."

--- a/src/FOL/simpdata.ML	Fri May 13 11:10:14 1994 +0200
+++ b/src/FOL/simpdata.ML	Fri May 13 11:25:55 1994 +0200
@@ -95,7 +95,9 @@
 val IFOL_ss = 
   empty_ss 
   setmksimps (map mk_meta_eq o atomize o gen_all)
-  setsolver  (fn prems => resolve_tac (triv_rls@prems) ORELSE' assume_tac)
+  setsolver  (fn prems => resolve_tac (triv_rls@prems) 
+	                  ORELSE' assume_tac
+	                  ORELSE' etac FalseE)
   setsubgoaler asm_simp_tac
   addsimps IFOL_rews
   addcongs [imp_cong];