| changeset 21888 | c75a44597fb7 |
| parent 20871 | da3a43cdbe8d |
| child 21900 | f386d7eb17d1 |
--- a/src/HOL/Tools/ATP/watcher.ML Tue Dec 19 19:34:35 2006 +0100 +++ b/src/HOL/Tools/ATP/watcher.ML Wed Dec 20 17:03:46 2006 +0100 @@ -23,7 +23,7 @@ (* Start a watcher and set up signal handlers*) val createWatcher : - thm * string Array.array list -> + thm * string Vector.vector list -> TextIO.instream * TextIO.outstream * Posix.Process.pid val killWatcher : Posix.Process.pid -> unit val killChild : ('a, 'b) Unix.proc -> OS.Process.status