diff -r 5f3cffe16311 -r 2f161c6910f7 src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Sun May 06 23:59:14 2018 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Tue May 08 10:32:07 2018 +0100
@@ -267,7 +267,7 @@
     and bdd_below_box[intro, simp]: "bdd_below (box a b)"
   unfolding atomize_conj
   by (metis bdd_above_Icc bdd_above_mono bdd_below_Icc bdd_below_mono bounded_box
-    bounded_subset_cbox interval_cbox)
+            bounded_subset_cbox_symmetric interval_cbox)
 
 instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
 begin