raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.

--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<midarrow>6, unary_ints, max_potential = 0,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 subsection {* Curry in a Hurry *}
 

--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<midarrow>8, max_potential = 0,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 primrec rot where
 "rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |

--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -13,7 +13,7 @@
 begin
 
 nitpick_params [verbose, max_potential = 0, sat_solver = MiniSat_JNI,
-                max_threads = 1, timeout = 120]
+                max_threads = 1, timeout = 240]
 
 typedecl guest
 typedecl key

--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<midarrow>8, unary_ints,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 inductive p1 :: "nat \<Rightarrow> bool" where
 "p1 0" |

--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<midarrow>5, bits = 1,2,3,4,6,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 lemma "Suc x = x + 1"
 nitpick [unary_ints, expect = none]

--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -18,7 +18,7 @@
 chapter {* 3. First Steps *}
 
 nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
-                timeout = 60]
+                timeout = 240]
 
 subsection {* 3.1. Propositional Logic *}
 

--- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 10, max_potential = 0, sat_solver = MiniSat_JNI,
-                max_threads = 1, timeout = 60]
+                max_threads = 1, timeout = 240]
 
 lemma "x = (case u of () \<Rightarrow> y)"
 nitpick [expect = genuine]

--- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 record point2d =
   xc :: int

--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 lemma "P \<and> Q"
 apply (rule conjI)

--- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 4, sat_solver = MiniSat_JNI, max_threads = 1,
-                timeout = 60]
+                timeout = 240]
 
 fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
 "f1 a b c d e = a + b + c + d + e"

--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1,
-                timeout = 60]
+                timeout = 240]
 
 typedef three = "{0\<Colon>nat, 1, 2}"
 by blast
@@ -159,7 +159,7 @@
 by (rule Rep_Nat_inverse)
 
 lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
-nitpick [card = 1, unary_ints, max_potential = 0, timeout = 240, expect = none]
+nitpick [card = 1, unary_ints, max_potential = 0, expect = none]
 by (rule Zero_int_def_raw)
 
 lemma "Abs_list (Rep_list a) = a"

--- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -2,7 +2,7 @@
 imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
 begin
 
-declare [[values_timeout = 240.0]]
+declare [[values_timeout = 480.0]]
 
 section {* Formal Languages *}
 

--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -2,7 +2,7 @@
 imports "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
 begin
 
-declare [[values_timeout = 240.0]]
+declare [[values_timeout = 480.0]]
 
 subsection {* Basic predicates *}