1.1 --- a/src/HOL/Tools/ATP/SpassCommunication.ML Wed Apr 20 22:43:52 2005 +0200
1.2 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML Thu Apr 21 10:05:06 2005 +0200
1.3 @@ -90,7 +90,7 @@
1.4
1.5 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
1.6 (* Attempt to prevent several signals from turning up simultaneously *)
1.7 - OS.Process.sleep(Time.fromSeconds 1)
1.8 + Posix.Process.sleep(Time.fromSeconds 1); ()
1.9
1.10 end
1.11
1.12 @@ -153,7 +153,7 @@
1.13 in if ( thisLine = "SPASS beiseite: Proof found.\n" )
1.14 then
1.15 (
1.16 - let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = OS.Process.sleep(Time.fromSeconds 3 );*)
1.17 + let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = Posix.Process.sleep(Time.fromSeconds 3 );*)
1.18 val _ = TextIO.output (outfile, (thisLine))
1.19
1.20 val _ = TextIO.closeOut outfile
1.21 @@ -165,7 +165,7 @@
1.22 then
1.23
1.24 (
1.25 - let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = OS.Process.sleep(Time.fromSeconds 3 );*)
1.26 + let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*)
1.27 val _ = TextIO.output (outfile, (thisLine))
1.28
1.29 val _ = TextIO.closeOut outfile
1.30 @@ -189,7 +189,7 @@
1.31 TextIO.flushOut toParent;
1.32 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
1.33 (* Attempt to prevent several signals from turning up simultaneously *)
1.34 - OS.Process.sleep(Time.fromSeconds 1);
1.35 + Posix.Process.sleep(Time.fromSeconds 1);
1.36 true
1.37 end)
1.38 else if ( thisLine = "SPASS beiseite: Ran out of time.\n" )
2.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Wed Apr 20 22:43:52 2005 +0200
2.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Apr 21 10:05:06 2005 +0200
2.3 @@ -15,7 +15,7 @@
2.4 (* Versions that include type information *)
2.5
2.6 fun string_of_thm thm = let val _ = set show_sorts
2.7 - val str = string_of_thm thm
2.8 + val str = Display.string_of_thm thm
2.9 val no_returns =List.filter not_newline (explode str)
2.10 val _ = reset show_sorts
2.11 in
2.12 @@ -222,9 +222,6 @@
2.13 (distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas)))
2.14 end
2.15
2.16 -fun thmstrings [] str = str
2.17 -| thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
2.18 -
2.19 fun numclstr (vars, []) str = str
2.20 | numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
2.21 in
3.1 --- a/src/HOL/Tools/ATP/watcher.ML Wed Apr 20 22:43:52 2005 +0200
3.2 +++ b/src/HOL/Tools/ATP/watcher.ML Thu Apr 21 10:05:06 2005 +0200
3.3 @@ -108,7 +108,7 @@
3.4
3.5 in
3.6 goals_being_watched := (!goals_being_watched) + 1;
3.7 - OS.Process.sleep(Time.fromSeconds 1);
3.8 + Posix.Process.sleep(Time.fromSeconds 1);
3.9 (warning ("probfile is: "^probfile));
3.10 (warning("dfg file is: "^newfile));
3.11 (warning ("wholefile is: "^(File.sysify_path wholefile)));
3.12 @@ -483,7 +483,7 @@
3.13 val parentID = Posix.ProcEnv.getppid()
3.14 val newProcList' =checkChildren (newProcList, toParentStr)
3.15 in
3.16 - (*OS.Process.sleep (Time.fromSeconds 1);*)
3.17 + (*Posix.Process.sleep (Time.fromSeconds 1);*)
3.18 loop (newProcList')
3.19 end
3.20 )
3.21 @@ -495,7 +495,7 @@
3.22 val parentID = Posix.ProcEnv.getppid()
3.23 val newProcList' =checkChildren (newProcList, toParentStr)
3.24 in
3.25 - (*OS.Process.sleep (Time.fromSeconds 1);*)
3.26 + (*Posix.Process.sleep (Time.fromSeconds 1);*)
3.27 loop (newProcList')
3.28 end
3.29 )
3.30 @@ -508,7 +508,7 @@
3.31 (******************************)
3.32 ( let val newProcList = checkChildren ((procList), toParentStr)
3.33 in
3.34 - OS.Process.sleep (Time.fromSeconds 1);
3.35 + Posix.Process.sleep (Time.fromSeconds 1);
3.36 loop (newProcList)
3.37 end
3.38