diff -r 4436039cc5e1 -r 1b39ba5db2c1 Nominal/Ex/CPS/CPS3_DanvyFilinski.thy --- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Fri Jul 22 11:52:12 2011 +0100 +++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Sun Jul 24 07:54:54 2011 +0200 @@ -217,7 +217,7 @@ apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) done -termination +termination (eqvt) by lexicographic_order definition psi:: "lt => lt"