--- a/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy Wed Nov 20 18:08:02 2013 +0100
+++ b/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy Wed Nov 20 18:09:23 2013 +0100
@@ -22,8 +22,8 @@
definition "Node n as \<equiv> NNode n (the_inv fset as)"
definition "cont \<equiv> fset o ccont"
-definition "unfold rt ct \<equiv> dtree_unfold rt (the_inv fset o ct)"
-definition "corec rt ct \<equiv> dtree_corec rt (the_inv fset o ct)"
+definition "unfold rt ct \<equiv> unfold_dtree rt (the_inv fset o ct)"
+definition "corec rt ct \<equiv> corec_dtree rt (the_inv fset o ct)"
lemma finite_cont[simp]: "finite (cont tr)"
unfolding cont_def o_apply by (cases tr, clarsimp)