# HG changeset patch
# User blanchet
# Date 1267007710 -3600
# Node ID c32d7269bad19925cd9b5a051ba6f94c722ad61b
# Parent  34819133c75e31f42c45c88d2c1d7ae19d1a76ab
compile

diff -r 34819133c75e -r c32d7269bad1 src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Feb 24 11:07:58 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Feb 24 11:35:10 2010 +0100
@@ -1418,10 +1418,6 @@
 nitpick [expect = genuine]
 oops
 
-lemma "P (x\<Colon>'a\<Colon>{classB, classE})"
-nitpick [expect = genuine]
-oops
-
 text {* OFCLASS: *}
 
 lemma "OFCLASS('a\<Colon>type, type_class)"