diff -r adfc759263ab -r 71c701dc5bf9 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 05 09:44:58 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 05 09:44:59 2013 +0100
@@ -2686,7 +2686,7 @@
 lemma Inf_insert:
   fixes S :: "real set"
   shows "bounded S \<Longrightarrow> Inf (insert x S) = (if S = {} then x else min x (Inf S))"
-  by (auto simp: bounded_imp_bdd_below inf_min cInf_insert_if)
+  by (auto simp: bounded_imp_bdd_below inf_min cInf_insert_If)
 
 lemma Inf_insert_finite:
   fixes S :: "real set"