src/HOL/ROOT

--- a/src/HOL/ROOT	Fri Feb 15 11:47:33 2013 +0100
+++ b/src/HOL/ROOT	Fri Feb 15 11:47:34 2013 +0100
@@ -20,18 +20,25 @@
   description {* Classical Higher-order Logic -- batteries included *}
   theories
     Library
-    Sublist
+    (*conflicting type class instantiations*)
     List_lexord
     Sublist_Order
-    Finite_Lattice
-    Code_Char
     Product_Lexorder
     Product_Order
+    Finite_Lattice
+    (*data refinements and dependent applications*)
+    AList_Mapping
+    Code_Binary_Nat
+    Code_Char
     (* Code_Prolog  FIXME cf. 76965c356d2a *)
     Code_Real_Approx_By_Float
     Code_Target_Numeral
-    IArray
+    DAList
+    RBT_Mapping
+    RBT_Set
+    (*legacy tools*)
     Refute
+    Old_Recdef
   theories [condition = ISABELLE_FULL_TEST]
     Sum_of_Squares_Remote
   files "document/root.bib" "document/root.tex"
@@ -148,7 +155,7 @@
 
 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
   options [document = false, document_graph = false, browser_info = false]
-  theories Generate Generate_Pretty RBT_Set_Test
+  theories Generate Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures Generate_Pretty_Char
 
 session "HOL-Metis_Examples" in Metis_Examples = HOL +
   description {*