src/HOL/BNF/More_BNFs.thy

--- a/src/HOL/BNF/More_BNFs.thy	Mon Jul 15 11:29:19 2013 +0200
+++ b/src/HOL/BNF/More_BNFs.thy	Mon Jul 15 14:23:51 2013 +0200
@@ -297,7 +297,7 @@
 
 lemma rcset_to_rcset: "countable A \<Longrightarrow> rcset (the_inv rcset A) = A"
 apply (rule f_the_inv_into_f)
-unfolding inj_on_def rcset_inj using rcset_surj by auto
+unfolding inj_on_def Rep_cset_inject using rcset_surj by auto
 
 lemma Collect_Int_Times:
 "{(x, y). R x y} \<inter> A \<times> B = {(x, y). R x y \<and> x \<in> A \<and> y \<in> B}"