--- a/Nominal/Nominal2_Supp.thy	Sat Mar 27 06:51:13 2010 +0100
+++ b/Nominal/Nominal2_Supp.thy	Sat Mar 27 08:11:11 2010 +0100
@@ -415,7 +415,7 @@
 apply(rule conjI)
 prefer 2
 apply(auto)[1]
-apply (metis left_minus minus_unique permute_atom_def_raw permute_minus_cancel(2))
+apply (metis permute_atom_def_raw permute_minus_cancel(2))
 defer
 apply(rule psubset_card_mono)
 apply(simp add: finite_supp)