src/HOL/Library/Permutation.thy
changeset 40122 1d8ad2ff3e01
parent 39916 8c83139a1433
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Library/Permutation.thy	Mon Oct 25 13:34:57 2010 +0200
     1.2 +++ b/src/HOL/Library/Permutation.thy	Mon Oct 25 13:34:58 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)