# HG changeset patch
# User blanchet
# Date 1409777225 -7200
# Node ID 7a259137a0baf4c3813180194a2e6cc246842fcc
# Parent  f04e24a24fb9d0824760ab0629a07fe88d0ee408
reenabled yet another example

diff -r f04e24a24fb9 -r 7a259137a0ba src/HOL/BNF_Examples/Misc_Datatype.thy
--- 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