--- a/src/Pure/simplifier.ML Tue Feb 10 14:29:36 2015 +0100
+++ b/src/Pure/simplifier.ML Tue Feb 10 14:48:26 2015 +0100
@@ -384,7 +384,7 @@
val trivialities = Drule.reflexive_thm :: trivs;
fun unsafe_solver_tac ctxt =
- FIRST' [resolve_tac (trivialities @ Raw_Simplifier.prems_of ctxt), assume_tac ctxt];
+ FIRST' [resolve_tac ctxt (trivialities @ Raw_Simplifier.prems_of ctxt), assume_tac ctxt];
val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
(*no premature instantiation of variables during simplification*)