src/HOL/Tools/res_atp.ML
changeset 21980 d22f7e3c5ad9
parent 21900 f386d7eb17d1
child 21999 0cf192e489e2
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Jan 03 18:29:46 2007 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Jan 03 18:30:57 2007 +0100
     1.3 @@ -894,9 +894,8 @@
     1.4             ignore (map (try cond_rm_tmp) files)))
     1.5       handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed";
     1.6  
     1.7 -(*writes out the current clasimpset to a tptp file;
     1.8 -  turns off xsymbol at start of function, restoring it at end    *)
     1.9 -fun isar_atp_body (ctxt, th) =
    1.10 +(*writes out the current problems and calls ATPs*)
    1.11 +fun isar_atp (ctxt, th) =
    1.12    if Thm.no_prems th then ()
    1.13    else
    1.14      let
    1.15 @@ -910,13 +909,11 @@
    1.16        watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
    1.17      end;
    1.18  
    1.19 -val isar_atp = setmp print_mode [] isar_atp_body;
    1.20 -
    1.21  (*For ML scripts, and primarily, for debugging*)
    1.22  fun callatp () =
    1.23    let val th = topthm()
    1.24        val ctxt = ProofContext.init (theory_of_thm th)
    1.25 -  in  isar_atp_body (ctxt, th)  end;
    1.26 +  in  isar_atp (ctxt, th)  end;
    1.27  
    1.28  val isar_atp_writeonly = setmp print_mode []
    1.29        (fn (ctxt,th) =>