--- a/src/HOL/Codatatype/Examples/HFset.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Examples/HFset.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Examples/HFset.thy
+(*  Title:      HOL/BNF/Examples/HFset.thy
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2012
 
@@ -8,7 +8,7 @@
 header {* Hereditary Sets *}
 
 theory HFset
-imports "../Codatatype"
+imports "../BNF"
 begin