# HG changeset patch
# User paulson
# Date 1145445095 -7200
# Node ID 651d949776f84b631c218283da12696fe623d78e
# Parent  b07e3bca20c94defb9cdb5dbdf5445f32af28a33
exported linkup_logic_mode and changed the default setting

diff -r b07e3bca20c9 -r 651d949776f8 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Wed Apr 19 10:43:53 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Wed Apr 19 13:11:35 2006 +0200
@@ -15,6 +15,7 @@
   val time_limit: int ref
    
   datatype mode = Auto | Fol | Hol
+  val linkup_logic_mode : mode ref
   val write_subgoal_file: mode -> Proof.context -> thm list -> thm list -> int -> string
   val vampire_time: int ref
   val eprover_time: int ref
@@ -339,7 +340,7 @@
 
 datatype mode = Auto | Fol | Hol;
 
-val linkup_logic_mode = ref Fol;
+val linkup_logic_mode = ref Auto;
 
 fun tptp_writer logic goals filename (axioms,classrels,arities) =
     if is_fol_logic logic