--- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy Mon Aug 18 17:19:58 2014 +0200
@@ -75,7 +75,7 @@
lemma unfold:
"root (unfold rt ct b) = rt b"
"finite (ct b) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> unfold rt ct) (ct b)"
-using dtree.sel_corec[of rt "the_inv fset o image (map_sum id Inr) o ct" b] unfolding unfold_def
+using dtree.corec_sel[of rt "the_inv fset o image (map_sum id Inr) o ct" b] unfolding unfold_def
apply blast
unfolding cont_def comp_def
by (simp add: case_sum_o_inj map_sum.compositionality image_image)
@@ -83,7 +83,7 @@
lemma corec:
"root (corec rt ct b) = rt b"
"finite (ct b) \<Longrightarrow> cont (corec rt ct b) = image (id \<oplus> ([[id, corec rt ct]])) (ct b)"
-using dtree.sel_corec[of rt "the_inv fset \<circ> ct" b] unfolding corec_def
+using dtree.corec_sel[of rt "the_inv fset \<circ> ct" b] unfolding corec_def
unfolding cont_def comp_def id_def
by simp_all