src/HOL/Finite_Set.thy

   assumes "finite A" and "x \<in> A"
   shows "F A = f x (F (A - {x}))"
 proof -
   from `x \<in> A` obtain B where A: "A = insert x B" and "x \<notin> B"
     by (auto dest: mk_disjoint_insert)
-  moreover from `finite A` this have "finite B" by simp
+  moreover from `finite A` A have "finite B" by simp
   ultimately show ?thesis by simp
 qed
 
 lemma insert_remove:
   assumes "finite A"