src/Pure/simplifier.ML
changeset 58957 c9e744ea8a38
parent 58048 aa6296d09e0e
child 58963 26bf09b95dda
     1.1 --- a/src/Pure/simplifier.ML	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -389,7 +389,7 @@
     1.4  
     1.5      (*no premature instantiation of variables during simplification*)
     1.6      fun safe_solver_tac ctxt =
     1.7 -      FIRST' [match_tac (trivialities @ Raw_Simplifier.prems_of ctxt), eq_assume_tac];
     1.8 +      FIRST' [match_tac ctxt (trivialities @ Raw_Simplifier.prems_of ctxt), eq_assume_tac];
     1.9      val safe_solver = mk_solver "easy safe" safe_solver_tac;
    1.10  
    1.11      fun mk_eq thm =