# HG changeset patch
# User lcp
# Date 785669021 -3600
# Node ID 436019ca97d7b22f39f813242aea7d57c7410cf1
# Parent  a8d1758bb1131e1feffddf803b36fd6e9073150e
cons_fun_eq: modified strange uses of classical reasoner

diff -r a8d1758bb113 -r 436019ca97d7 src/ZF/func.ML
--- a/src/ZF/func.ML	Thu Nov 24 00:33:13 1994 +0100
+++ b/src/ZF/func.ML	Thu Nov 24 10:23:41 1994 +0100
@@ -380,12 +380,13 @@
 (*For Finite.ML.  Inclusion of right into left is easy*)
 goal ZF.thy
     "!!c. c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})";
-by (safe_tac (eq_cs addSEs [fun_extend3]));
+by (rtac equalityI 1);
+by (safe_tac (ZF_cs addSEs [fun_extend3]));
 (*Inclusion of left into right*)
 by (subgoal_tac "restrict(x, A) : A -> B" 1);
 by (fast_tac (ZF_cs addEs [restrict_type2]) 2);
 by (rtac UN_I 1 THEN assume_tac 1);
-by (rtac UN_I 1 THEN fast_tac (ZF_cs addEs [apply_type]) 1);
+by (rtac (apply_funtype RS UN_I) 1 THEN REPEAT (ares_tac [consI1] 1));
 by (simp_tac (FOL_ss addsimps cons_iff::mem_simps) 1);
 by (resolve_tac [fun_extension] 1 THEN REPEAT (ares_tac [fun_extend] 1));
 by (etac consE 1);