src/Sequents/simpdata.ML

--- a/src/Sequents/simpdata.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Sequents/simpdata.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -58,7 +58,7 @@
   @{thm iff_refl}, reflexive_thm];
 
 fun unsafe_solver ctxt =
-  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), assume_tac];
+  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), assume_tac ctxt];
 
 (*No premature instantiation of variables during simplification*)
 fun safe_solver ctxt =