# HG changeset patch
# User lcp
# Date 768821155 -7200
# Node ID 3a853818f1d224c1ea4da956fef8c865826e6ee3
# Parent  e95e212512d18ed8f73222eda6c945e1cfea7d24
FOL/simpdata: added etac FalseE in setsolver call.  Toby: "now that the
simplifier can rewrite premises, it can generate the premise False."

diff -r e95e212512d1 -r 3a853818f1d2 src/FOL/simpdata.ML
--- 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];