clarified timeout for isatest;

--- a/Admin/isatest/isatest-makeall	Mon Sep 22 21:31:45 2014 +0200
+++ b/Admin/isatest/isatest-makeall	Mon Sep 22 21:45:59 2014 +0200
@@ -87,10 +87,10 @@
 
     case "$SETTINGS" in
       *sml*)
-        BUILD_ARGS="-o timeout=36000 $BUILD_ARGS"
+        BUILD_ARGS="-o timeout=54000 $BUILD_ARGS"
         ;;
       *)
-        BUILD_ARGS="-o timeout=3600 $BUILD_ARGS"
+        BUILD_ARGS="-o timeout=5400 $BUILD_ARGS"
         ;;
     esac
 

--- a/src/HOL/ROOT	Mon Sep 22 21:31:45 2014 +0200
+++ b/src/HOL/ROOT	Mon Sep 22 21:45:59 2014 +0200
@@ -19,7 +19,7 @@
   description {*
     HOL-Main with explicit proof terms.
   *}
-  options [timeout = 5400, document = false]
+  options [document = false]
   theories Proofs (*sequential change of global flag!*)
   theories "~~/src/HOL/Library/Old_Datatype"
   files
@@ -260,7 +260,7 @@
 
     Testing Metis and Sledgehammer.
   *}
-  options [timeout = 3600, document = false]
+  options [document = false]
   theories
     Abstraction
     Big_O
@@ -522,7 +522,7 @@
   description {*
     Miscellaneous examples for Higher-Order Logic.
   *}
-  options [timeout = 3600, condition = ML_SYSTEM_POLYML]
+  options [condition = ML_SYSTEM_POLYML]
   theories [document = false]
     "~~/src/HOL/Library/State_Monad"
     Code_Binary_Nat_examples
@@ -722,7 +722,7 @@
   theories Nominal
 
 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
-  options [timeout = 3600, condition = ML_SYSTEM_POLYML, document = false]
+  options [condition = ML_SYSTEM_POLYML, document = false]
   theories
     Nominal_Examples_Base
   theories [condition = ISABELLE_FULL_TEST]