# HG changeset patch
# User blanchet
# Date 1268391742 -3600
# Node ID c910fe606829b08298470dcd12b9cfb573f38b9b
# Parent  19eefc0655b64de18ee77527d7258c3b73d37019
make tests less demanding, to prevent sporadic failures

diff -r 19eefc0655b6 -r c910fe606829 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Mar 11 23:47:16 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Mar 12 12:02:22 2010 +0100
@@ -464,13 +464,13 @@
 theorem dataset_skew_split:
 "dataset (skew t) = dataset t"
 "dataset (split t) = dataset t"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
 sorry
 
 theorem wf_skew_split:
 "wf t \<Longrightarrow> skew t = t"
 "wf t \<Longrightarrow> split t = t"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
 sorry
 
 primrec insort\<^isub>1 where
@@ -494,11 +494,11 @@
                        (if x > y then insort\<^isub>2 u x else u))"
 
 theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
 sorry
 
 theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
 sorry
 
 end