--- a/src/HOL/Library/Permutation.thy Mon Oct 04 12:22:58 2010 +0200
+++ b/src/HOL/Library/Permutation.thy Mon Oct 04 14:46:48 2010 +0200
@@ -168,7 +168,7 @@
apply simp
apply (subgoal_tac "a#list <~~> a#ysa@zs")
apply (metis Cons_eq_appendI perm_append_Cons trans)
- apply (metis Cons Cons_eq_appendI distinct.simps(2)
+ apply (metis Cons Cons_eq_appendI distinct_simps(2)
distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
apply (fastsimp simp add: insert_ident)