diff -r f122140b7195 -r c09598a97436 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Jul 18 21:25:55 2015 +0200
+++ b/src/Provers/classical.ML	Sat Jul 18 21:44:18 2015 +0200
@@ -157,7 +157,7 @@
       val rule'' =
         rule' |> ALLGOALS (SUBGOAL (fn (goal, i) =>
           if i = 1 orelse redundant_hyp goal
-          then eresolve0_tac [thin_rl] i
+          then eresolve_tac ctxt [thin_rl] i
           else all_tac))
         |> Seq.hd
         |> Drule.zero_var_indexes;