diff -r 8355a6e2df79 -r 293ab573d034 src/HOL/ROOT
--- a/src/HOL/ROOT	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/ROOT	Sat Dec 17 15:22:13 2016 +0100
@@ -31,18 +31,14 @@
   *}
   theories
     Library
-    Nonpos_Ints
-    Periodic_Fun
     Polynomial_Factorial
-    Predicate_Compile_Quickcheck
+    (*conflicting type class instantiations and dependent applications*)
+    Finite_Lattice
+    List_lexord
     Prefix_Order
-    Rewrite
-    (*conflicting type class instantiations*)
-    List_lexord
-    Sublist_Order
     Product_Lexorder
     Product_Order
-    Finite_Lattice
+    Sublist_Order
     (*data refinements and dependent applications*)
     AList_Mapping
     Code_Binary_Nat
@@ -54,11 +50,13 @@
     DAList_Multiset
     RBT_Mapping
     RBT_Set
+    (*prototypic tools*)
+    Predicate_Compile_Quickcheck
     (*legacy tools*)
-    Refute
     Old_Datatype
     Old_Recdef
     Old_SMT
+    Refute
   document_files "root.bib" "root.tex"
 
 session "HOL-Hahn_Banach" in Hahn_Banach = HOL +