1.1 --- a/src/HOL/Proofs/Lambda/Eta.thy	Mon Mar 26 18:32:22 2012 +0200
     1.2 +++ b/src/HOL/Proofs/Lambda/Eta.thy	Mon Mar 26 19:03:27 2012 +0200
     1.3 @@ -159,7 +159,7 @@
     1.4       apply (slowsimp intro: rtrancl_eta_subst eta_subst)
     1.5      apply (blast intro: rtrancl_eta_AppL)
     1.6     apply (blast intro: rtrancl_eta_AppR)
     1.7 -  apply simp;
     1.8 +  apply simp
     1.9    apply (slowsimp intro: rtrancl_eta_Abs free_beta
    1.10      iff del: dB.distinct simp: dB.distinct)    (*23 seconds?*)
    1.11    done