src/HOL/Library/Poly_Mapping.thy

 lemma items_the_value:
   assumes "sorted (List.map fst xs)" and "distinct (List.map fst xs)" and "0 \<notin> snd ` set xs"
   shows "items (the_value xs) = xs"
 proof -
   from assms have "sorted_list_of_set (set (List.map fst xs)) = List.map fst xs"
-    unfolding sorted_list_of_set_sort_remdups by (simp add: distinct_remdups_id sorted_sort_id)
+    unfolding sorted_list_of_set_sort_remdups by (simp add: distinct_remdups_id sort_key_id_if_sorted)
   moreover from assms have "keys (the_value xs) = fst ` set xs"
     by transfer (auto simp add: image_def split: option.split dest: set_map_of_compr)
   ultimately show ?thesis
     unfolding items_def using assms
     by (auto simp add: lookup_the_value intro: map_idI)