diff -r ec7cc76e88e5 -r f4579e6800d7 src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Tue Nov 12 12:33:05 2019 +0000
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Nov 14 11:54:52 2019 +0100
@@ -698,10 +698,10 @@
 
 lemmas independent_imp_finite = finiteI_independent
 
-corollary
+corollary\<^marker>\<open>tag unimportant\<close> independent_card_le:
   fixes S :: "'a::euclidean_space set"
   assumes "independent S"
-  shows independent_card_le:"card S \<le> DIM('a)"
+  shows "card S \<le> DIM('a)"
   using assms independent_bound by auto
 
 lemma dependent_biggerset: