src/HOL/Real/HahnBanach/HahnBanach.thy

   interpret normed_vectorspace_with_fn_norm [E norm B fn_norm]
     by (auto simp: B_def fn_norm_def) intro_locales
   interpret subspace [F E] by fact
   interpret linearform [F f] by fact
   interpret continuous [F norm f] by fact
-  have E: "vectorspace E" by unfold_locales
-  have F: "vectorspace F" by rule unfold_locales
+  have E: "vectorspace E" by intro_locales
+  have F: "vectorspace F" by rule intro_locales
   have F_norm: "normed_vectorspace F norm"
     using FE E_norm by (rule subspace_normed_vs)
   have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
     by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero
       [OF normed_vectorspace_with_fn_norm.intro,