reintroduce example (cf. 39281b3e4fac)
authortraytel
Thu, 10 Apr 2014 11:34:55 +0200
changeset 56488 535cfc7fc301
parent 56487 961b34963fa4
child 56515 b62c4e6d1b55
reintroduce example (cf. 39281b3e4fac)
src/HOL/BNF_Examples/Compat.thy
--- a/src/HOL/BNF_Examples/Compat.thy	Thu Apr 10 10:52:48 2014 +0200
+++ b/src/HOL/BNF_Examples/Compat.thy	Thu Apr 10 11:34:55 2014 +0200
@@ -69,7 +69,7 @@
 datatype fnky = Fnky "nat tre"
 
 datatype_new tree = Tree "tree foo"
-(* FIXME: datatype_compat tree *)
+datatype_compat tree
 
 ML {* Datatype_Data.get_info @{theory} @{type_name tree} *}