# HG changeset patch
# User blanchet
# Date 1384967363 -3600
# Node ID 69b3ff79a69ecbc72869091ac22fd5e304ae133f
# Parent  59737a43e044fa162368b858470db3421cd16775
compile

diff -r 59737a43e044 -r 69b3ff79a69e src/HOL/BNF/Examples/Derivation_Trees/DTree.thy
--- 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)