--- a/src/HOL/TPTP/atp_problem_import.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML Fri Oct 31 11:36:41 2014 +0100
@@ -117,7 +117,7 @@
if falsify then "CounterSatisfiable" else "Satisfiable"
else
"Unknown")
- |> Output.urgent_message
+ |> writeln
val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
val params =
[("maxtime", string_of_int timeout),
@@ -135,7 +135,7 @@
fun SOLVE_TIMEOUT seconds name tac st =
let
- val _ = Output.urgent_message ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
+ val _ = writeln ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
val result =
TimeLimit.timeLimit (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
handle
@@ -143,8 +143,8 @@
| ERROR _ => NONE
in
(case result of
- NONE => (Output.urgent_message ("FAILURE: " ^ name); Seq.empty)
- | SOME st' => (Output.urgent_message ("SUCCESS: " ^ name); Seq.single st'))
+ NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
+ | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
end
fun nitpick_finite_oracle_tac ctxt timeout i th =
@@ -264,7 +264,7 @@
Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => @{prop False})
fun print_szs_of_success conjs success =
- Output.urgent_message ("% SZS status " ^
+ writeln ("% SZS status " ^
(if success then
if null conjs then "Unsatisfiable" else "Theorem"
else