diff -r 633ccbcd8d8c -r abd760a19e22 src/HOL/BNF/Examples/TreeFI.thy
--- a/src/HOL/BNF/Examples/TreeFI.thy	Mon Aug 12 23:21:06 2013 +0200
+++ b/src/HOL/BNF/Examples/TreeFI.thy	Mon Aug 12 23:36:43 2013 +0200
@@ -19,11 +19,7 @@
 by (auto simp add: listF.set_map')
 
 lemma dtor[simp]: "treeFI_dtor tr = (lab tr, sub tr)"
-unfolding lab_def sub_def treeFI_case_def
-(*
-by (metis fst_def pair_collapse snd_def)
-*)
-sorry
+by (metis Tree_def treeFI.collapse treeFI.dtor_ctor)
 
 definition pair_fun (infixr "\<odot>" 50) where
   "f \<odot> g \<equiv> \<lambda>x. (f x, g x)"