src/HOL/Vector_Spaces.thy

   shows "\<lbrakk>S \<subseteq> T; dim T \<le> dim S\<rbrakk> \<Longrightarrow> span S = span T"
   by (simp add: span_mono subspace_dim_equal)
 
 lemma dim_psubset:
   "span S \<subset> span T \<Longrightarrow> dim S < dim T"
-  by (metis (no_types, hide_lams) dim_span less_le not_le subspace_dim_equal subspace_span)
+  by (metis (no_types, opaque_lifting) dim_span less_le not_le subspace_dim_equal subspace_span)
 
 lemma dim_eq_full:
   shows "dim S = dimension \<longleftrightarrow> span S = UNIV"
   by (metis dim_eq_span dim_subset_UNIV span_Basis span_span subset_UNIV
         dim_UNIV dim_span dimension_def)