diff --git a/thys/Irrational_Series_Erdos_Straus/ROOT b/thys/Irrational_Series_Erdos_Straus/ROOT
--- a/thys/Irrational_Series_Erdos_Straus/ROOT
+++ b/thys/Irrational_Series_Erdos_Straus/ROOT
@@ -1,13 +1,10 @@
-chapter AFP
-
-session Irrational_Series_Erdos_Straus = "HOL-Analysis" +
-  options [timeout = 1200]
-  sessions
-    Prime_Number_Theorem
-    Prime_Distribution_Elementary
-  theories
-    Irrational_Series_Erdos_Straus
-  document_files
-    "root.tex"
-    "root.bib"
-
+chapter AFP
+
+session Irrational_Series_Erdos_Straus = Prime_Distribution_Elementary +
+  options [timeout = 300]
+  theories
+    Irrational_Series_Erdos_Straus
+  document_files
+    "root.tex"
+    "root.bib"
+