1.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Mon Feb 22 14:36:10 2010 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Mon Feb 22 19:31:00 2010 +0100
     1.3 @@ -11,7 +11,8 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
     1.8 +nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
     1.9 +                timeout = 60 s]
    1.10  
    1.11  primrec rot where
    1.12  "rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
    1.13 @@ -27,9 +28,8 @@
    1.14  
    1.15  lemma "rot Nibble2 \<noteq> Nibble3"
    1.16  nitpick [card = 1, expect = none]
    1.17 -nitpick [card = 2, expect = genuine]
    1.18 +nitpick [card = 2, max Nibble4 = 0, expect = genuine]
    1.19  nitpick [card = 2, max Nibble2 = 0, expect = none]
    1.20 -nitpick [card = 2, max Nibble3 = 0, expect = none]
    1.21  oops
    1.22  
    1.23  lemma "(rot ^^ 15) n \<noteq> n"
    1.24 @@ -53,7 +53,7 @@
    1.25  "sn (Pd (_, b)) = b"
    1.26  
    1.27  lemma "fs (Pd p) = fst p"
    1.28 -nitpick [card = 20, expect = none]
    1.29 +nitpick [card = 12, expect = none]
    1.30  sorry
    1.31  
    1.32  lemma "fs (Pd p) = snd p"
    1.33 @@ -61,7 +61,7 @@
    1.34  oops
    1.35  
    1.36  lemma "sn (Pd p) = snd p"
    1.37 -nitpick [card = 20, expect = none]
    1.38 +nitpick [card = 12, expect = none]
    1.39  sorry
    1.40  
    1.41  lemma "sn (Pd p) = fst p"
    1.42 @@ -69,7 +69,7 @@
    1.43  oops
    1.44  
    1.45  lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
    1.46 -nitpick [card = 1\<midarrow>12, expect = none]
    1.47 +nitpick [card = 1\<midarrow>10, expect = none]
    1.48  sorry
    1.49  
    1.50  lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
    1.51 @@ -82,7 +82,7 @@
    1.52  "app (Fn f) x = f x"
    1.53  
    1.54  lemma "app (Fn g) y = g y"
    1.55 -nitpick [card = 1\<midarrow>12, expect = none]
    1.56 +nitpick [card = 1\<midarrow>10, expect = none]
    1.57  sorry
    1.58  
    1.59  lemma "app (Fn g) y = g' y"