src/HOL/BNF_Def.thy

--- a/src/HOL/BNF_Def.thy	Mon Jun 26 23:12:43 2017 +0200
+++ b/src/HOL/BNF_Def.thy	Tue Jun 27 00:07:34 2017 +0200
@@ -82,7 +82,7 @@
   "vimage2p f g R = (\<lambda>x y. R (f x) (g y))"
 
 lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)"
-  by (rule ext) (auto simp only: comp_apply collect_def)
+  by (rule ext) (simp add: collect_def)
 
 definition convol ("\<langle>(_,/ _)\<rangle>") where
   "\<langle>f, g\<rangle> \<equiv> \<lambda>a. (f a, g a)"