# HG changeset patch
# User blanchet
# Date 1409777225 -7200
# Node ID 08052d9f805035296ab1573b3ae5c324130f5e6a
# Parent  86a374caeb8213d3b9e741cd2f1796b38532cb2f
reenabled example

diff -r 86a374caeb82 -r 08052d9f8050 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
@@ -207,11 +207,8 @@
 instance tree' and branch :: (countable) countable
   by countable_datatype
 
-(* FIXME:
-
 instance bin_rose_tree :: (countable) countable
   by countable_datatype
-*)
 
 instance exp and trm and factor :: (countable, countable) countable
   by countable_datatype