--- a/src/Pure/simplifier.ML Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Pure/simplifier.ML Mon Nov 10 21:49:48 2014 +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];
+ FIRST' [resolve_tac (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*)