1.1 --- a/src/HOL/List.thy	Mon Apr 30 12:14:51 2012 +0200
     1.2 +++ b/src/HOL/List.thy	Mon Apr 30 12:14:53 2012 +0200
     1.3 @@ -4483,7 +4483,7 @@
     1.4      \<and> distinct (sorted_list_of_set A)"
     1.5    by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)
     1.6  
     1.7 -lemma sorted_list_of_set_sort_remdups:
     1.8 +lemma sorted_list_of_set_sort_remdups [code]:
     1.9    "sorted_list_of_set (set xs) = sort (remdups xs)"
    1.10  proof -
    1.11    interpret comp_fun_commute insort by (fact comp_fun_commute_insort)