# HG changeset patch
# User paulson
# Date 1160487205 -7200
# Node ID 3bbe7cab80373693bae98feda7c97a00c9efc1b4
# Parent  1ea394dc2a0fccdff52ce540c212a0b2f9fc8370
A way to call the ATP linkup from ML scripts

diff -r 1ea394dc2a0f -r 3bbe7cab8037 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Tue Oct 10 15:30:48 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Tue Oct 10 15:33:25 2006 +0200
@@ -5,7 +5,7 @@
 ATPs with TPTP format input.
 *)
 
-(*FIXME: Do we need this signature?*)
+(*Currently unused, during debugging*)
 signature RES_ATP =
 sig
   val prover: string ref
@@ -829,8 +829,7 @@
 
 (*writes out the current clasimpset to a tptp file;
   turns off xsymbol at start of function, restoring it at end    *)
-val isar_atp = setmp print_mode [] 
- (fn (ctxt, th) =>
+fun isar_atp_body (ctxt, th) =
   if Thm.no_prems th then ()
   else
     let
@@ -842,7 +841,15 @@
       Output.debug ("problem files: " ^ space_implode ", " files); 
       Output.debug ("pid: " ^ string_of_pid pid);
       watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
-    end);
+    end;
+
+val isar_atp = setmp print_mode [] isar_atp_body;
+
+(*For ML scripts, and primarily, for debugging*)
+fun callatp () = 
+  let val th = topthm()
+      val ctxt = ProofContext.init (theory_of_thm th)
+  in  isar_atp_body (ctxt, th)  end;
 
 val isar_atp_writeonly = setmp print_mode [] 
       (fn (ctxt,th) =>