--- a/Quot/Nominal/Terms.thy	Mon Feb 08 10:47:19 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Mon Feb 08 11:41:25 2010 +0100
@@ -214,16 +214,16 @@
 as
   "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
 
+lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted]
+
 instance
 apply default
 apply(induct_tac [!] x rule: trm1_bp_inducts(1))
-apply(simp_all add: permute_rtrm1_permute_bp.simps[quot_lifted])
+apply(simp_all)
 done
 
 end
 
-lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted]
-
 lemmas fv_trm1 = rfv_trm1_rfv_bp.simps[quot_lifted]
 
 lemmas fv_trm1_eqvt = rfv_trm1_eqvt[quot_lifted]