# HG changeset patch
# User blanchet
# Date 1346666061 -7200
# Node ID d2ed455fa3d2a9ee82dc96ba4952f7f7eea30343
# Parent  ed769978dc8d6cab4ef5d539de51579b8edc3ba0
compile

diff -r ed769978dc8d -r d2ed455fa3d2 src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy
--- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy	Mon Sep 03 11:54:21 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy	Mon Sep 03 11:54:21 2012 +0200
@@ -15,7 +15,7 @@
 
 typedecl N  typedecl T
 
-bnf_codata Tree: 'Tree = "N \<times> (T + 'Tree) fset"
+codata_raw Tree: 'Tree = "N \<times> (T + 'Tree) fset"
 
 
 section {* Sugar notations for Tree *}