diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/ROOT	Mon Jan 20 18:24:56 2014 +0100
@@ -699,13 +699,6 @@
     "document/root.tex"
     "document/root.bib"
 
-session "HOL-BNF" in BNF = HOL +
-  description {*
-    Bounded Natural Functors for (Co)datatypes, Including More BNFs.
-  *}
-  options [document = false]
-  theories BNF
-
 session "HOL-BNF_Examples" in BNF_Examples = HOL +
   description {*
     Examples for Bounded Natural Functors.