--- a/src/HOL/BNF_Examples/Misc_Datatype.thy Wed Sep 03 22:47:05 2014 +0200
+++ b/src/HOL/BNF_Examples/Misc_Datatype.thy Wed Sep 03 22:47:05 2014 +0200
@@ -216,11 +216,8 @@
instance nofail1 :: (countable) countable
by countable_datatype
-(* FIXME:
-
instance nofail2 :: (countable) countable
by countable_datatype
-*)
(* TODO: Enable once "fset" is registered as countable:
@@ -231,7 +228,7 @@
by countable_datatype
instance l1 and l2 :: countable
- by default (rule l1_countable)
+ by countable_datatype
*)
instance kk1 and kk2 :: countable