diff -r 02c88bdabe75 -r 5b45125b15ba src/HOL/List.thy
--- a/src/HOL/List.thy	Sat May 14 00:32:16 2011 +0200
+++ b/src/HOL/List.thy	Sat May 14 18:26:25 2011 +0200
@@ -3765,7 +3765,7 @@
 lemma fun_left_comm_insort:
   "fun_left_comm insort"
 proof
-qed (fact insort_left_comm)
+qed (simp add: insort_left_comm fun_eq_iff)
 
 lemma sort_key_simps [simp]:
   "sort_key f [] = []"