src/HOL/Library/Permutation.thy
changeset 39916 8c83139a1433
parent 39078 39f8f6d1eb74
child 40122 1d8ad2ff3e01
     1.1 --- a/src/HOL/Library/Permutation.thy	Mon Oct 04 12:22:58 2010 +0200
     1.2 +++ b/src/HOL/Library/Permutation.thy	Mon Oct 04 14:46:48 2010 +0200
     1.3 @@ -168,7 +168,7 @@
     1.4      apply simp
     1.5      apply (subgoal_tac "a#list <~~> a#ysa@zs")
     1.6       apply (metis Cons_eq_appendI perm_append_Cons trans)
     1.7 -    apply (metis Cons Cons_eq_appendI distinct.simps(2)
     1.8 +    apply (metis Cons Cons_eq_appendI distinct_simps(2)
     1.9        distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
    1.10     apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
    1.11      apply (fastsimp simp add: insert_ident)