src/Provers/quantifier1.ML
changeset 7951 b36913c35699
parent 4319 afb60b8bf15e
child 11221 60c6e91f6079
--- 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