1.1 --- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Tue Feb 23 11:05:32 2010 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Tue Feb 23 12:14:29 2010 +0100
     1.3 @@ -110,12 +110,12 @@
     1.4  
     1.5  lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}.
     1.6         f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
     1.7 -nitpick [expect = potential] (* unfortunate *)
     1.8 +nitpick [expect = genuine]
     1.9  oops
    1.10  
    1.11  lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}.
    1.12         f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
    1.13 -nitpick [expect = potential] (* unfortunate *)
    1.14 +nitpick [expect = genuine]
    1.15  oops
    1.16  
    1.17  lemma "\<forall>a. g a = a