--- a/src/HOL/Library/Countable_Set_Type.thy Tue Feb 09 07:04:32 2016 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy Tue Feb 09 07:04:48 2016 +0100
@@ -472,7 +472,8 @@
lemma cUnion_parametric [transfer_rule]:
"(rel_cset (rel_cset A) ===> rel_cset A) cUnion cUnion"
- unfolding rel_fun_def by transfer(simp, fast dest: rel_setD1 rel_setD2 intro!: rel_setI)
+ unfolding rel_fun_def
+ by transfer (auto simp: rel_set_def, metis+)
lemma cimage_parametric [transfer_rule]:
"((A ===> B) ===> rel_cset A ===> rel_cset B) cimage cimage"