# HG changeset patch
# User nipkow
# Date 941037448 -7200
# Node ID b36913c356995d39e52abf657c4182f68d219b08
# Parent  720af28e635490a84174a5a7a8624a3168894a1a
Fixed a bug in the EX simproc.

diff -r 720af28e6354 -r b36913c35699 src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Wed Oct 27 17:09:31 1999 +0200
+++ b/src/Provers/quantifier1.ML	Wed Oct 27 17:17:28 1999 +0200
@@ -102,9 +102,10 @@
           in Some(prove_conv prove_all_tac sg (F,all$Abs(x,T,R))) end)
   | rearrange_all _ _ _ = None;
 
+(* Better: instantiate exI *)
 val prove_ex_tac = rtac iffI 1 THEN
-    ALLGOALS(EVERY'[etac exE, REPEAT o (etac conjE),
-                    rtac exI, REPEAT o (ares_tac [conjI] ORELSE' etac sym)]);
+    ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
+                    DEPTH_SOLVE_1 o (ares_tac [conjI] APPEND' etac sym)]);
 
 fun rearrange_ex sg _ (F as ex $ Abs(x,T,P)) =
      (case extract P of