--- a/src/HOL/Codatatype/Examples/Misc_Codata.thy Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Codata.thy Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Codatatype/Examples/Misc_Data.thy
+(* Title: HOL/BNF/Examples/Misc_Data.thy
Author: Dmitriy Traytel, TU Muenchen
Author: Andrei Popescu, TU Muenchen
Copyright 2012
@@ -9,7 +9,7 @@
header {* Miscellaneous Codatatype Declarations *}
theory Misc_Codata
-imports "../Codatatype"
+imports "../BNF"
begin
codata simple = X1 | X2 | X3 | X4