# HG changeset patch
# User blanchet
# Date 1267008952 -3600
# Node ID 4dc65845eab3f426e7816a7807a1f55845387eaf
# Parent  c6bbfa9c4eca6b17f2b4f69be5bbca25a7585eda
compile

diff -r c6bbfa9c4eca -r 4dc65845eab3 src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Feb 24 11:35:39 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Feb 24 11:55:52 2010 +0100
@@ -1430,12 +1430,6 @@
 apply intro_classes
 done
 
-lemma "OFCLASS('a, classB_class)"
-nitpick [expect = none]
-apply intro_classes
-apply simp
-done
-
 lemma "OFCLASS('a\<Colon>type, classC_class)"
 nitpick [expect = genuine]
 oops