diff -r 0c5cd369a643 -r 50b60f501b05 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/Pure/raw_simplifier.ML	Tue Feb 10 14:48:26 2015 +0100
@@ -1309,7 +1309,7 @@
   in bottomc (mode, Option.map (Drule.flexflex_unique (SOME ctxt)) oo prover, maxidx) ctxt ct end;
 
 val simple_prover =
-  SINGLE o (fn ctxt => ALLGOALS (resolve_tac (prems_of ctxt)));
+  SINGLE o (fn ctxt => ALLGOALS (resolve_tac ctxt (prems_of ctxt)));
 
 fun rewrite _ _ [] = Thm.reflexive
   | rewrite ctxt full thms =