diff -r c958f282b382 -r 55e798614c45 src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy
--- a/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy	Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy	Wed Sep 26 10:01:00 2012 +0200
@@ -177,7 +177,7 @@
 theorem TTree_unfold:
 "root (TTree_unfold rt ct b) = rt b"
 "ccont (TTree_unfold rt ct b) = map_fset (id \<oplus> TTree_unfold rt ct) (ct b)"
-using Tree.dtor_unfolds[of "<rt,ct>" b] unfolding Tree_unfold_unfold fst_convol snd_convol
+using Tree.dtor_unfold[of "<rt,ct>" b] unfolding Tree_unfold_unfold fst_convol snd_convol
 unfolding pre_Tree_map' fst_convol' snd_convol'
 unfolding Tree_dtor_root_ccont by simp_all
 
@@ -194,7 +194,7 @@
 theorem TTree_corec:
 "root (TTree_corec rt ct b) = rt b"
 "ccont (TTree_corec rt ct b) = map_fset (id \<oplus> ([[id, TTree_corec rt ct]]) ) (ct b)"
-using Tree.dtor_corecs[of "<rt,ct>" b] unfolding Tree_dtor_corec_corec fst_convol snd_convol
+using Tree.dtor_corec[of "<rt,ct>" b] unfolding Tree_dtor_corec_corec fst_convol snd_convol
 unfolding pre_Tree_map' fst_convol' snd_convol'
 unfolding Tree_dtor_root_ccont by simp_all