1.1 --- a/src/HOL/Library/Countable.thy	Thu Nov 12 17:21:48 2009 +0100
     1.2 +++ b/src/HOL/Library/Countable.thy	Thu Nov 12 17:21:51 2009 +0100
     1.3 @@ -165,7 +165,7 @@
     1.4  text {* Lists *}
     1.5  
     1.6  lemma from_nat_to_nat_map [simp]: "map from_nat (map to_nat xs) = xs"
     1.7 -  by (simp add: comp_def map_compose [symmetric])
     1.8 +  by (simp add: comp_def)
     1.9  
    1.10  primrec
    1.11    list_encode :: "'a\<Colon>countable list \<Rightarrow> nat"