diff -r 59203adfc33f -r ccda99401bc8 src/HOL/Tools/sat.ML
--- a/src/HOL/Tools/sat.ML	Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/sat.ML	Thu Oct 30 22:45:19 2014 +0100
@@ -406,7 +406,7 @@
 
 fun rawsat_tac ctxt i =
   Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
-    rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i;
+    resolve_tac [rawsat_thm ctxt' (map cprop_of prems)] 1) ctxt i;
 
 (* ------------------------------------------------------------------------- *)
 (* pre_cnf_tac: converts the i-th subgoal                                    *)
@@ -421,7 +421,7 @@
 (* ------------------------------------------------------------------------- *)
 
 fun pre_cnf_tac ctxt =
-  rtac @{thm ccontr} THEN'
+  resolve_tac @{thms ccontr} THEN'
   Object_Logic.atomize_prems_tac ctxt THEN'
   CONVERSION Drule.beta_eta_conversion;
 
@@ -433,7 +433,7 @@
 (* ------------------------------------------------------------------------- *)
 
 fun cnfsat_tac ctxt i =
-  (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i);
+  (eresolve_tac [FalseE] i) ORELSE (REPEAT_DETERM (eresolve_tac [conjE] i) THEN rawsat_tac ctxt i);
 
 (* ------------------------------------------------------------------------- *)
 (* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
@@ -443,8 +443,8 @@
 (* ------------------------------------------------------------------------- *)
 
 fun cnfxsat_tac ctxt i =
-  (etac FalseE i) ORELSE
-    (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i);
+  (eresolve_tac [FalseE] i) ORELSE
+    (REPEAT_DETERM (eresolve_tac [conjE] i ORELSE eresolve_tac [exE] i) THEN rawsat_tac ctxt i);
 
 (* ------------------------------------------------------------------------- *)
 (* sat_tac: tactic for calling an external SAT solver, taking as input an    *)