diff -r b8c227d8ca91 -r c95319d14332 src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Thu Feb 15 12:02:11 2007 +0100
+++ b/src/HOL/FunDef.thy	Thu Feb 15 12:14:34 2007 +0100
@@ -126,5 +126,9 @@
   \<Longrightarrow> split f p = split g q"
   by (auto simp:split_def)
 
+lemma comp_cong[fundef_cong]:
+  "f (g x) = f' (g' x')
+  ==>  (f o g) x = (f' o g') x'"
+unfolding o_apply .
 
 end