More blacklisting
CASC mode now always on, due to switch to Vampire 8.1 (i.e. the 2006 version)
Now runs ATPs unless time_limit = 0.

--- a/src/HOL/Tools/res_atp.ML	Wed Nov 01 08:46:54 2006 +0100
+++ b/src/HOL/Tools/res_atp.ML	Wed Nov 01 15:39:20 2006 +0100
@@ -302,6 +302,7 @@
   an attribute.*)
 val blacklist = ref
   ["Datatype.prod.size",
+   "Datatype.unit.exhaust", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*)
    "Datatype.unit.induct", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*)
    "Datatype.unit.inducts",
    "Datatype.unit.split_asm", 
@@ -732,8 +733,7 @@
             else if !prover = "vampire"
 	    then 
               let val vampire = helper_path "VAMPIRE_HOME" "vampire"
-                  val casc = if !time_limit > 70 then "--mode casc%" else ""
-                  val vopts = casc ^ "-m 100000%-t " ^ time
+                  val vopts = "--mode casc%-t " ^ time  (*what about -m 100000?*)
               in
                   ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
               end
@@ -874,8 +874,8 @@
     Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
     ResClause.init thy;
     ResHolClause.init thy;
-    if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal)
-    else isar_atp_writeonly (ctxt, goal)
+    if !time_limit > 0 then isar_atp (ctxt, goal)
+    else (warning "Writing problem file only"; isar_atp_writeonly (ctxt, goal))
   end;
 
 val invoke_atp = Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep