--- a/src/ZF/domrange.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/domrange.ML Thu Sep 26 15:14:23 1996 +0200
@@ -79,7 +79,7 @@
qed_goalw "range_subset" ZF.thy [range_def] "range(A*B) <= B"
(fn _ =>
- [ (rtac (converse_prod RS ssubst) 1),
+ [ (stac converse_prod 1),
(rtac domain_subset 1) ]);