# HG changeset patch
# User paulson
# Date 861785569 -7200
# Node ID 65778b9d865fb705853be774adeb136bc1dd1f1d
# Parent  f5554654d211d41b7b64b31aab99f96a14168989
Ran expandshort

diff -r f5554654d211 -r 65778b9d865f src/ZF/mono.ML
--- a/src/ZF/mono.ML	Wed Apr 23 10:49:01 1997 +0200
+++ b/src/ZF/mono.ML	Wed Apr 23 10:52:49 1997 +0200
@@ -180,13 +180,13 @@
 val [PQimp] = goal IFOL.thy
     "[| !!x. P(x) --> Q(x) |] ==> (EX x.P(x)) --> (EX x.Q(x))";
 by IntPr.safe_tac;
-be (PQimp RS mp RS exI) 1;
+by (etac (PQimp RS mp RS exI) 1);
 qed "ex_mono";
 
 val [PQimp] = goal IFOL.thy
     "[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))";
 by IntPr.safe_tac;
-be (spec RS (PQimp RS mp)) 1;
+by (etac (spec RS (PQimp RS mp)) 1);
 qed "all_mono";
 
 (*Used in intr_elim.ML and in individual datatype definitions*)