# HG changeset patch
# User bulwahn
# Date 1335780893 -7200
# Node ID 179b5e7c980300f0d5710a14c2e05302678c46cc
# Parent  732ea1f08e3f0091d1d91a164f91f9f5df30d672
making sorted_list_of_set executable

diff -r 732ea1f08e3f -r 179b5e7c9803 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Apr 30 12:14:51 2012 +0200
+++ b/src/HOL/List.thy	Mon Apr 30 12:14:53 2012 +0200
@@ -4483,7 +4483,7 @@
     \<and> distinct (sorted_list_of_set A)"
   by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)
 
-lemma sorted_list_of_set_sort_remdups:
+lemma sorted_list_of_set_sort_remdups [code]:
   "sorted_list_of_set (set xs) = sort (remdups xs)"
 proof -
   interpret comp_fun_commute insort by (fact comp_fun_commute_insort)