# HG changeset patch
# User immler@in.tum.de
# Date 1246194088 -7200
# Node ID db3f00a39edd1c417ef22baacc083c37db0a1eb6
# Parent  28f5ed40ecabfc3c9dca562ad6a05e15e4c3cb1e
fixed

diff -r 28f5ed40ecab -r db3f00a39edd src/HOL/Tools/atp_wrapper.ML
--- a/src/HOL/Tools/atp_wrapper.ML	Sat Jun 27 22:28:07 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML	Sun Jun 28 15:01:28 2009 +0200
@@ -146,7 +146,7 @@
                ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
   timeout;
 
-val vampire_full = vampire_opts 60 false;
+val vampire_full = vampire_opts_full 60 false;
 
 
 (* E prover *)