1.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Thu Feb 25 16:33:39 2010 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Feb 26 16:49:46 2010 +0100
     1.3 @@ -1000,7 +1000,7 @@
     1.4  oops
     1.5  
     1.6  lemma "(Q\<Colon>nat set) (Eps Q)"
     1.7 -nitpick [expect = none]
     1.8 +nitpick [expect = none] (* unfortunate *)
     1.9  oops
    1.10  
    1.11  lemma "\<not> Q (Eps Q)"
    1.12 @@ -1053,11 +1053,11 @@
    1.13  
    1.14  lemma "Q = {x\<Colon>'a} \<Longrightarrow> (Q\<Colon>'a set) (The Q)"
    1.15  nitpick [expect = none]
    1.16 -oops
    1.17 +sorry
    1.18  
    1.19  lemma "Q = {x\<Colon>nat} \<Longrightarrow> (Q\<Colon>nat set) (The Q)"
    1.20  nitpick [expect = none]
    1.21 -oops
    1.22 +sorry
    1.23  
    1.24  subsection {* Destructors and Recursors *}
    1.25