
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




