# HG changeset patch
# User paulson
# Date 903022158 -7200
# Node ID 3e14d6d66dab7d0e67387ffde57341385769baea
# Parent  01c2b317da884a039d6495ce0ef56f3e91729a5e
Blast_tac is faster

diff -r 01c2b317da88 -r 3e14d6d66dab src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Thu Aug 13 17:28:52 1998 +0200
+++ b/src/FOL/ROOT.ML	Thu Aug 13 17:29:18 1998 +0200
@@ -55,7 +55,7 @@
 
 qed_goal "ex1_functional" FOL.thy
     "!!a b c. [| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
- (fn _ => [ (deepen_tac FOL_cs 0 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 
 print_depth 8;