--- 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]: