src/HOL/Tools/res_atp.ML
changeset 17488 67376a311a2b
parent 17484 f6a225f97f0a
child 17502 8836793df947
     1.1 --- a/src/HOL/Tools/res_atp.ML	Mon Sep 19 16:42:11 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Sep 19 18:30:22 2005 +0200
     1.3 @@ -201,12 +201,10 @@
     1.4        val _ = debug ("claset and simprules total clauses = " ^ 
     1.5                       string_of_int (Array.length clause_arr))
     1.6        val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr)
     1.7 -      val pid_string =
     1.8 -        string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid)))
     1.9      in
    1.10        debug ("initial thms: " ^ thms_string);
    1.11        debug ("subgoals: " ^ prems_string);
    1.12 -      debug ("pid: "^ pid_string);
    1.13 +      debug ("pid: " ^ Int.toString (ResLib.intOfPid pid));
    1.14        write_problem_files axclauses thm (length prems);
    1.15        watcher_call_provers (sign_of_thm thm) (Thm.prems_of thm) (childin, childout, pid)
    1.16      end);