src/FOL/simpdata.ML
changeset 58838 59203adfc33f
parent 56245 84fc7dfa3cd4
child 58957 c9e744ea8a38
     1.1 --- a/src/FOL/simpdata.ML	Thu Oct 30 16:20:46 2014 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Thu Oct 30 16:55:29 2014 +0100
     1.3 @@ -107,7 +107,9 @@
     1.4  val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}];
     1.5  
     1.6  fun unsafe_solver ctxt =
     1.7 -  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), atac, etac @{thm FalseE}];
     1.8 +  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt),
     1.9 +    assume_tac,
    1.10 +    eresolve_tac @{thms FalseE}];
    1.11  
    1.12  (*No premature instantiation of variables during simplification*)
    1.13  fun safe_solver ctxt =