--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Sat Feb 13 11:56:06 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Sat Feb 13 15:04:09 2010 +0100
@@ -259,7 +259,7 @@
(if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
"swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
-lemma "\<lbrakk>a \<in> labels t; b \<in> labels t; a \<noteq> b\<rbrakk> \<Longrightarrow> labels (swap t a b) = labels t"
+lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t"
nitpick
proof (induct t)
case Leaf thus ?case by simp