src/ZF/func.ML

--- a/src/ZF/func.ML	Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/func.ML	Thu Sep 26 15:14:23 1996 +0200
@@ -184,7 +184,7 @@
     "(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)";
 by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1);
 by (rtac ballI 1);
-by (rtac (beta RS ssubst) 1);
+by (stac beta 1);
 by (assume_tac 1);
 by (etac (major RS theI) 1);
 qed "lam_theI";