Tuned uniqueness proof for recursion combinator.

--- a/src/HOL/Nominal/nominal_package.ML	Mon Jan 28 18:17:42 2008 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Mon Jan 28 18:18:19 2008 +0100
@@ -1907,8 +1907,9 @@
                           (HOLogic.mk_Trueprop (fresh_const aT rT $ b $ lhs'))
                           (fn _ => EVERY
                              [cut_facts_tac [th'] 1,
-                              NominalPermeq.perm_simp_tac (HOL_ss addsimps
-                                (rec_eqns @ pi1_pi2_eqs @ perm_swap)) 1,
+                              full_simp_tac (Simplifier.theory_context thy11 HOL_ss
+                                addsimps rec_eqns @ pi1_pi2_eqs @ perm_swap
+                                addsimprocs [NominalPermeq.perm_simproc_app]) 1,
                               full_simp_tac (HOL_ss addsimps (calc_atm @
                                 fresh_prems' @ freshs2' @ perm_fresh_fresh)) 1])
                       end;