diff -r 59203adfc33f -r ccda99401bc8 src/HOL/Tools/cnf.ML
--- a/src/HOL/Tools/cnf.ML	Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/cnf.ML	Thu Oct 30 22:45:19 2014 +0100
@@ -141,7 +141,7 @@
       if i > nprems_of thm then
         thm
       else
-        not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm))
+        not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (resolve_tac [clause2raw_not_disj] i) thm))
     (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *)
     (* becomes "[..., A1, ..., An] |- B"                                   *)
     (* Thm.thm -> Thm.thm *)
@@ -154,7 +154,7 @@
     (* [...] |- ~x1 ==> ... ==> ~xn ==> False *)
     |> not_disj_to_prem 1
     (* [...] |- x1' ==> ... ==> xn' ==> False *)
-    |> Seq.hd o TRYALL (rtac clause2raw_not_not)
+    |> Seq.hd o TRYALL (resolve_tac [clause2raw_not_not])
     (* [..., x1', ..., xn'] |- False *)
     |> prems_to_hyps
   end;
@@ -529,7 +529,7 @@
 (* ------------------------------------------------------------------------- *)
 
 fun weakening_tac i =
-  dtac weakening_thm i THEN atac (i+1);
+  dresolve_tac [weakening_thm] i THEN assume_tac (i+1);
 
 (* ------------------------------------------------------------------------- *)
 (* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF       *)