diff -r 38c0bbb8348b -r 21dac9a60f0c src/HOL/BNF/Examples/Derivation_Trees/DTree.thy
--- a/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy	Tue Oct 01 17:04:27 2013 +0200
+++ b/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy	Tue Oct 01 17:06:35 2013 +0200
@@ -26,14 +26,14 @@
 definition "corec rt ct \<equiv> dtree_corec rt (the_inv fset o ct)"
 
 lemma finite_cont[simp]: "finite (cont tr)"
-  unfolding cont_def o_apply by (cases tr, clarsimp) (transfer, simp)
+  unfolding cont_def o_apply by (cases tr, clarsimp)
 
 lemma Node_root_cont[simp]:
   "Node (root tr) (cont tr) = tr"
   unfolding Node_def cont_def o_apply
   apply (rule trans[OF _ dtree.collapse])
   apply (rule arg_cong2[OF refl the_inv_into_f_f[unfolded inj_on_def]])
-  apply transfer apply simp_all
+  apply (simp_all add: fset_inject)
   done
 
 lemma dtree_simps[simp]: