diff -r 57e781b711b5 -r 5c9819d7713b src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/ROOT	Mon Nov 18 18:04:45 2013 +0100
@@ -687,21 +687,14 @@
   theories Nominal_Examples
   theories [quick_and_dirty] VC_Condition
 
-session "HOL-Cardinals-LFP" in Cardinals = HOL +
+session "HOL-Cardinals-FP" in Cardinals = HOL +
   description {*
-    Ordinals and Cardinals, Theories Needed for BNF LFP Construction.
+    Ordinals and Cardinals, Theories Needed for BNF FP Constructions.
   *}
   options [document = false]
-  theories Cardinal_Arithmetic_LFP
+  theories Cardinal_Arithmetic_FP
 
-session "HOL-Cardinals-GFP" in Cardinals = "HOL-Cardinals-LFP" +
-  description {*
-    Ordinals and Cardinals, Theories Needed for BNF GFP Construction.
-  *}
-  options [document = false]
-  theories Cardinal_Arithmetic_GFP
-
-session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-GFP" +
+session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-FP" +
   description {*
     Ordinals and Cardinals, Full Theories.
   *}
@@ -712,23 +705,16 @@
     "document/root.tex"
     "document/root.bib"
 
-session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-LFP" +
+session "HOL-BNF-FP" in BNF = "HOL-Cardinals-FP" +
   description {*
-    Bounded Natural Functors for Datatypes.
+    Bounded Natural Functors for (Co)datatypes.
   *}
   options [document = false]
-  theories BNF_LFP
+  theories BNF_LFP BNF_GFP
 
-session "HOL-BNF-GFP" in BNF = "HOL-Cardinals-GFP" +
+session "HOL-BNF" in BNF = "HOL-BNF-FP" +
   description {*
-    Bounded Natural Functors for Codatatypes.
-  *}
-  options [document = false]
-  theories BNF_GFP
-
-session "HOL-BNF" in BNF = "HOL-Cardinals-GFP" +
-  description {*
-    Bounded Natural Functors for (Co)datatypes.
+    Bounded Natural Functors for (Co)datatypes, Including More BNFs.
   *}
   options [document = false]
   theories BNF