src/HOL/Finite.ML

   by (etac (rewrite_rule [inj_on_def] finite_imageD) 1);
   by (simp_tac (simpset() addsplits [split_split]) 1);
  by (etac finite_imageI 1);
 by (simp_tac (simpset() addsimps [converse_def,image_def]) 1);
 by Auto_tac;
- by (rtac bexI 1);
- by (assume_tac 2);
+by (rtac bexI 1);
+by  (assume_tac 2);
 by (Simp_tac 1);
 qed "finite_converse";
 AddIffs [finite_converse];
 
 section "Finite cardinality -- 'card'";