diff -r 7641e8d831d2 -r 01e968432467 src/HOL/Library/AssocList.thy
--- a/src/HOL/Library/AssocList.thy	Thu Feb 18 14:21:44 2010 -0800
+++ b/src/HOL/Library/AssocList.thy	Thu Feb 18 14:28:26 2010 -0800
@@ -688,6 +688,10 @@
   "Mapping.keys (AList xs) = set (map fst xs)"
   by (simp add: keys_def dom_map_of_conv_image_fst)
 
+lemma ordered_keys_AList [code]:
+  "Mapping.ordered_keys (AList xs) = sort (remdups (map fst xs))"
+  by (simp only: ordered_keys_def keys_AList sorted_list_of_set_sort_remdups)
+
 lemma size_AList [code]:
   "Mapping.size (AList xs) = length (remdups (map fst xs))"
   by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)