src/HOL/Library/Countable.thy

       in
         SOLVED' (fn i => EVERY
           [rtac @{thm countable_datatype} i,
            rtac typedef_thm i,
            etac induct_thm' i,
-           REPEAT (resolve_tac rules i ORELSE atac i)]) 1
+           REPEAT (resolve_tac ctxt rules i ORELSE atac i)]) 1
       end)
 *}
 
 hide_const (open) finite_item nth_item