diff -r 1ff66e72628b -r 39281b3e4fac src/HOL/BNF_Examples/Compat.thy
--- a/src/HOL/BNF_Examples/Compat.thy	Tue Apr 08 18:16:47 2014 +0200
+++ b/src/HOL/BNF_Examples/Compat.thy	Tue Apr 08 18:48:10 2014 +0200
@@ -2,11 +2,10 @@
 imports Main
 begin
 
-
 datatype_new 'a lst = Nl | Cns 'a "'a lst"
 datatype_compat lst
 
-datatype_new 'b w = W | W' "'b w * 'b list"
+datatype_new 'b w = W | W' "'b w \<times> 'b list"
 (* no support for sums of products
 datatype_compat w
 *)
@@ -70,7 +69,7 @@
 datatype fnky = Fnky "nat tre"
 
 datatype_new tree = Tree "tree foo"
-datatype_compat tree
+(* FIXME: datatype_compat tree *)
 
 ML {* Datatype_Data.get_info @{theory} @{type_name tree} *}