--- a/Nominal-General/Nominal2_Supp.thy	Wed Apr 21 12:38:20 2010 +0200
+++ b/Nominal-General/Nominal2_Supp.thy	Wed Apr 21 16:24:18 2010 +0200
@@ -433,6 +433,13 @@
   qed
 qed
 
+lemma perm_struct_induct2[case_names zero swap]:
+  assumes zero: "P 0"
+  assumes swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
+  shows "P p"
+by (rule_tac S="supp p" in perm_struct_induct)
+   (auto intro: zero swap)
+
 lemma perm_subset_induct [consumes 1, case_names zero swap plus]:
   assumes S: "supp p \<subseteq> S"
   assumes zero: "P 0"