1.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Feb 24 11:35:39 2010 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Feb 24 11:55:52 2010 +0100
     1.3 @@ -1430,12 +1430,6 @@
     1.4  apply intro_classes
     1.5  done
     1.6  
     1.7 -lemma "OFCLASS('a, classB_class)"
     1.8 -nitpick [expect = none]
     1.9 -apply intro_classes
    1.10 -apply simp
    1.11 -done
    1.12 -
    1.13  lemma "OFCLASS('a\<Colon>type, classC_class)"
    1.14  nitpick [expect = genuine]
    1.15  oops