src/HOL/List.thy

--- a/src/HOL/List.thy	Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/List.thy	Wed Feb 17 21:51:56 2016 +0100
@@ -6774,7 +6774,7 @@
 
 lemma set_relcomp [code]:
   "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
-  by (auto simp add: Bex_def)
+  by auto (auto simp add: Bex_def image_def)
 
 lemma wf_set [code]:
   "wf (set xs) = acyclic (set xs)"