src/HOL/Analysis/Cross3.thy

--- a/src/HOL/Analysis/Cross3.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Cross3.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -100,7 +100,7 @@
 
 lemma  cross_basis_nonzero:
   "u \<noteq> 0 \<Longrightarrow> u \<times> axis 1 1 \<noteq> 0 \<or> u \<times> axis 2 1 \<noteq> 0 \<or> u \<times> axis 3 1 \<noteq> 0"
-  by (clarsimp simp add: axis_def cross3_simps) (metis vector_3 exhaust_3)
+  by (clarsimp simp add: axis_def cross3_simps) (metis exhaust_3)
 
 lemma  cross_dot_cancel:
   fixes x::"real^3"