# HG changeset patch
# User blanchet
# Date 1260783095 -3600
# Node ID 61b7aa37f4b75610b2210e196b46d81aba5735c0
# Parent  bb01fd325c6b0a327a28c2de75a89acabb6c1c25
make Nitpick "Core" test more conservative, to avoid problems on Larry's machine

diff -r bb01fd325c6b -r 61b7aa37f4b7 src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Dec 14 10:13:06 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Dec 14 10:31:35 2009 +0100
@@ -11,6 +11,8 @@
 imports Main
 begin
 
+nitpick_params [sat_solver = MiniSatJNI]
+
 subsection {* Curry in a Hurry *}
 
 lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
@@ -135,7 +137,7 @@
 by (auto simp: Id_def Collect_def)
 
 lemma "Id ((a\<Colon>'a, b\<Colon>'a), (a, b))"
-nitpick [card = 1\<midarrow>20, expect = none]
+nitpick [card = 1\<midarrow>10, expect = none]
 by (auto simp: Id_def Collect_def)
 
 lemma "UNIV (x\<Colon>'a\<times>'a)"