diff -r 2c65870c706f -r e20a999f7161 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Thu Jul 17 10:29:09 2014 +0200
+++ b/src/HOL/Library/Tree.thy	Thu Jul 17 14:55:56 2014 +0200
@@ -10,6 +10,7 @@
   where
     "left Leaf = Leaf"
   | "right Leaf = Leaf"
+datatype_compat tree
 
 lemma neq_Leaf_iff: "(t \<noteq> Leaf) = (\<exists>l a r. t = Node l a r)"
   by (cases t) auto