src/FOL/simpdata.ML
changeset 58957 c9e744ea8a38
parent 58838 59203adfc33f
child 58963 26bf09b95dda
     1.1 --- a/src/FOL/simpdata.ML	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -113,7 +113,8 @@
     1.4  
     1.5  (*No premature instantiation of variables during simplification*)
     1.6  fun safe_solver ctxt =
     1.7 -  FIRST' [match_tac (triv_rls @ Simplifier.prems_of ctxt), eq_assume_tac, ematch_tac @{thms FalseE}];
     1.8 +  FIRST' [match_tac ctxt (triv_rls @ Simplifier.prems_of ctxt),
     1.9 +    eq_assume_tac, ematch_tac ctxt @{thms FalseE}];
    1.10  
    1.11  (*No simprules, but basic infastructure for simplification*)
    1.12  val FOL_basic_ss =