diff -r b73f7e42135e -r 1c0926788772 src/ZF/domrange.ML
--- a/src/ZF/domrange.ML	Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/domrange.ML	Thu Sep 30 10:10:21 1993 +0100
@@ -174,7 +174,7 @@
     (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
 
 val image_subset = prove_goal ZF.thy
-    "!!A B r. [| r <= A*B;  C<=A |] ==> r``C <= B"
+    "!!A B r. r <= A*B ==> r``C <= B"
  (fn _ =>
   [ (rtac subsetI 1),
     (REPEAT (eresolve_tac [asm_rl, imageE, subsetD RS SigmaD2] 1)) ]);
@@ -202,8 +202,8 @@
     (REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ]);
 
 val vimage_subset = prove_goalw ZF.thy [vimage_def]
-    "!!A B r. [| r <= A*B;  C<=B |] ==> r-``C <= A"
- (fn _ => [ (REPEAT (ares_tac [converse_type RS image_subset] 1)) ]);
+    "!!A B r. r <= A*B ==> r-``C <= A"
+ (fn _ => [ (etac (converse_type RS image_subset) 1) ]);
 
 
 (** Theorem-proving for ZF set theory **)