src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Sat Nov 09 00:12:25 2002 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Nov 13 15:24:42 2002 +0100
@@ -304,7 +304,7 @@
    apply (rule trancl_subset_Field2 [THEN finite_subset])
    apply (rule finite_SigmaI)
     prefer 3
-    apply (blast intro: r_into_trancl finite_subset)
+    apply (blast intro: r_into_trancl' finite_subset)
    apply (auto simp add: finite_Field)
   done