--- a/src/HOL/Library/Permutation.thy Tue Mar 18 20:33:29 2008 +0100
+++ b/src/HOL/Library/Permutation.thy Tue Mar 18 20:33:31 2008 +0100
@@ -188,7 +188,7 @@
apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
apply (fastsimp simp add: insert_ident)
apply (metis distinct_remdups set_remdups)
- apply (metis Nat.le_less_trans Suc_length_conv length_remdups_leq less_Suc_eq nat_less_le)
+ apply (metis le_less_trans Suc_length_conv length_remdups_leq less_Suc_eq nat_less_le)
done
lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"