# HG changeset patch
# User blanchet
# Date 1289035508 -3600
# Node ID 8adcdd2c5805faaa5421a08841196ae98cae78f0
# Parent  3642dc3b72e8fa20232d7b0c9c71973507330385
make Nitpick datatype tests faster to make timeout less likely

diff -r 3642dc3b72e8 -r 8adcdd2c5805 src/HOL/Nitpick_Examples/Datatype_Nits.thy
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Sat Nov 06 10:25:08 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Sat Nov 06 10:25:08 2010 +0100
@@ -23,7 +23,7 @@
 "rot NibbleF = Nibble0"
 
 lemma "rot n \<noteq> n"
-nitpick [card = 1\<midarrow>16, expect = none]
+nitpick [card = 1\<midarrow>8,16, verbose, expect = none]
 sorry
 
 lemma "rot Nibble2 \<noteq> Nibble3"
@@ -69,7 +69,7 @@
 oops
 
 lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
-nitpick [card = 1\<midarrow>9, expect = none]
+nitpick [expect = none]
 sorry
 
 lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
@@ -82,7 +82,7 @@
 "app (Fn f) x = f x"
 
 lemma "app (Fn g) y = g y"
-nitpick [card = 1\<midarrow>10, expect = none]
+nitpick [expect = none]
 sorry
 
 lemma "app (Fn g) y = g' y"