# 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;