diff -r a594429637fd -r fdd6989cc8a0 Admin/isatest/isatest-makeall
--- a/Admin/isatest/isatest-makeall	Wed Feb 17 21:08:18 2016 +0100
+++ b/Admin/isatest/isatest-makeall	Wed Feb 17 23:06:24 2016 +0100
@@ -24,7 +24,7 @@
   echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
   echo
   echo "Examples:"
-  echo "  $PRG ~/settings/at-poly ~/settings/at-sml"
+  echo "  $PRG ~/settings/at-poly"
   echo "  $PRG -l \"HOL-Library HOL-Bali\" ~/settings/at-poly"
   exit 1
 }
@@ -92,14 +92,7 @@
 
     [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
 
-    case "$SETTINGS" in
-      *sml*)
-        BUILD_ARGS="-o timeout=72000 $BUILD_ARGS"
-        ;;
-      *)
-        BUILD_ARGS="-o timeout=10800 $BUILD_ARGS"
-        ;;
-    esac
+    BUILD_ARGS="-o timeout=10800 $BUILD_ARGS"
 
     # logfile setup