diff -r 903c956beac3 -r d80e9aeb4a2b src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Mon Sep 21 12:01:14 1998 +0200
+++ b/src/HOL/Finite.ML	Mon Sep 21 15:58:27 1998 +0200
@@ -187,8 +187,8 @@
  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];