diff -r 0c5cd369a643 -r 50b60f501b05 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/FOL/simpdata.ML	Tue Feb 10 14:48:26 2015 +0100
@@ -23,7 +23,7 @@
 (*Replace premises x=y, X<->Y by X==Y*)
 fun mk_meta_prems ctxt =
     rule_by_tactic ctxt
-      (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
+      (REPEAT_FIRST (resolve_tac ctxt [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
 
 (*Congruence rules for = or <-> (instead of ==)*)
 fun mk_meta_cong ctxt rl =
@@ -107,9 +107,9 @@
 val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}];
 
 fun unsafe_solver ctxt =
-  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt),
+  FIRST' [resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt),
     assume_tac ctxt,
-    eresolve_tac @{thms FalseE}];
+    eresolve_tac ctxt @{thms FalseE}];
 
 (*No premature instantiation of variables during simplification*)
 fun safe_solver ctxt =