diff -r 81ada90d8220 -r 960f0a4404c7 src/HOL/Proofs/Lambda/Eta.thy
--- a/src/HOL/Proofs/Lambda/Eta.thy	Mon Mar 26 18:32:22 2012 +0200
+++ b/src/HOL/Proofs/Lambda/Eta.thy	Mon Mar 26 19:03:27 2012 +0200
@@ -159,7 +159,7 @@
      apply (slowsimp intro: rtrancl_eta_subst eta_subst)
     apply (blast intro: rtrancl_eta_AppL)
    apply (blast intro: rtrancl_eta_AppR)
-  apply simp;
+  apply simp
   apply (slowsimp intro: rtrancl_eta_Abs free_beta
     iff del: dB.distinct simp: dB.distinct)    (*23 seconds?*)
   done