--- a/src/HOL/Codatatype/Examples/TreeFsetI.thy Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Codatatype/Examples/TreeFsetI.thy
+(* Title: HOL/BNF/Examples/TreeFsetI.thy
Author: Dmitriy Traytel, TU Muenchen
Author: Andrei Popescu, TU Muenchen
Copyright 2012
@@ -9,7 +9,7 @@
header {* Finitely Branching Possibly Infinite Trees, with Sets of Children *}
theory TreeFsetI
-imports "../Codatatype"
+imports "../BNF"
begin
hide_const (open) Sublist.sub