src/HOL/Library/Countable.thy
changeset 28823 dcbef866c9e2
parent 27487 c8a6ce181805
child 29511 7071b017cb35
--- a/src/HOL/Library/Countable.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Library/Countable.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -49,7 +49,7 @@
   by (rule countable_classI [of "id"]) simp 
 
 subclass (in finite) countable
-proof unfold_locales
+proof
   have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV)
   with finite_conv_nat_seg_image [of UNIV]
   obtain n and f :: "nat \<Rightarrow> 'a"