src/HOL/List.thy

 
 definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
   "sorted_list_of_set = folding.F insort []"
 
 sublocale sorted_list_of_set!: folding insort Nil
-where
+rewrites
   "folding.F insort [] = sorted_list_of_set"
 proof -
   interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
   show "folding insort" by standard (fact comp_fun_commute)
   show "folding.F insort [] = sorted_list_of_set" by (simp only: sorted_list_of_set_def)