src/HOL/HOLCF/Tools/cont_proc.ML

--- a/src/HOL/HOLCF/Tools/cont_proc.ML	Sat Jul 18 20:53:05 2015 +0200
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Sat Jul 18 20:54:56 2015 +0200
@@ -102,7 +102,7 @@
     fun new_cont_tac f' i =
       case all_cont_thms f' of
         [] => no_tac
-      | (c::_) => rtac c i
+      | (c::_) => resolve_tac ctxt [c] i
 
     fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) =
       let