# HG changeset patch
# User berghofe
# Date 1201540699 -3600
# Node ID f38dc602a926f711af2e10a036e5d0f501a7a0fb
# Parent  0c0f5d990d7d1fcaeac3fb0290b9f6c6f37bb803
Tuned uniqueness proof for recursion combinator.

diff -r 0c0f5d990d7d -r f38dc602a926 src/HOL/Nominal/nominal_package.ML
--- 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;