Theorem "arctan" is no longer a default simprule

--- a/src/HOL/Library/ContNotDenum.thy	Wed Apr 01 15:47:55 2015 +0100
+++ b/src/HOL/Library/ContNotDenum.thy	Wed Apr 01 16:04:21 2015 +0100
@@ -110,7 +110,7 @@
 qed
 
 lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV"
-  using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan_tan)
+  using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan)
 
 lemma uncountable_open_interval:
   fixes a b :: real assumes ab: "a < b"