1.1 --- a/src/HOL/Nominal/Nominal.thy	Mon Sep 22 15:26:14 2008 +0200
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Mon Sep 22 19:46:24 2008 +0200
     1.3 @@ -3495,12 +3495,12 @@
     1.4    {* NominalPermeq.perm_simp_meth_debug *}
     1.5    {* simp rules and simprocs for analysing permutations including debugging facilities *}
     1.6  
     1.7 -method_setup perm_full_simp =
     1.8 -  {* NominalPermeq.perm_full_simp_meth *}
     1.9 +method_setup perm_extend_simp =
    1.10 +  {* NominalPermeq.perm_extend_simp_meth *}
    1.11    {* tactic for deciding equalities involving permutations *}
    1.12  
    1.13 -method_setup perm_full_simp_debug =
    1.14 -  {* NominalPermeq.perm_full_simp_meth_debug *}
    1.15 +method_setup perm_extend_simp_debug =
    1.16 +  {* NominalPermeq.perm_extend_simp_meth_debug *}
    1.17    {* tactic for deciding equalities involving permutations including debugging facilities *}
    1.18  
    1.19  method_setup supports_simp =