1.1 --- a/src/HOL/List.thy	Sat May 14 00:32:16 2011 +0200
     1.2 +++ b/src/HOL/List.thy	Sat May 14 18:26:25 2011 +0200
     1.3 @@ -3765,7 +3765,7 @@
     1.4  lemma fun_left_comm_insort:
     1.5    "fun_left_comm insort"
     1.6  proof
     1.7 -qed (fact insort_left_comm)
     1.8 +qed (simp add: insort_left_comm fun_eq_iff)
     1.9  
    1.10  lemma sort_key_simps [simp]:
    1.11    "sort_key f [] = []"