--- a/src/HOL/Complex/ex/BigO_Complex.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Complex/ex/BigO_Complex.thy	Wed May 07 10:57:19 2008 +0200
@@ -42,7 +42,7 @@
   apply (drule set_plus_imp_minus)
   apply (drule bigo_LIMSEQ1)
   apply assumption
-  apply (simp only: func_diff)
+  apply (simp only: fun_diff_def)
   apply (erule LIMSEQ_diff_approach_zero2)
   apply assumption
 done