
diff -r 4b198af5beb5 -r c57dba973391 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- 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




