# HG changeset patch
# User paulson
# Date 1114070706 -7200
# Node ID 8fad4bd4e53cf227e86c5f78330148aba1970b5e
# Parent  81e9f17823eac71499f182ee670911b9b2eee8d3
improved SML/NJ compatibility, etc.

diff -r 81e9f17823ea -r 8fad4bd4e53c src/HOL/Tools/ATP/SpassCommunication.ML
--- a/src/HOL/Tools/ATP/SpassCommunication.ML	Wed Apr 20 22:43:52 2005 +0200
+++ b/src/HOL/Tools/ATP/SpassCommunication.ML	Thu Apr 21 10:05:06 2005 +0200
@@ -90,7 +90,7 @@
                                           
                                          Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
                                          (* Attempt to prevent several signals from turning up simultaneously *)
-                                         OS.Process.sleep(Time.fromSeconds 1)
+                                         Posix.Process.sleep(Time.fromSeconds 1); ()
                                                
                                     end
                                       
@@ -153,7 +153,7 @@
                                            in if ( thisLine = "SPASS beiseite: Proof found.\n" )
                                               then      
                                               (  
-                                                 let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                      (*val _ =  OS.Process.sleep(Time.fromSeconds 3 );*)
+                                                 let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                                                (*val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
                                                      val _ = TextIO.output (outfile, (thisLine))
                                              
                                                      val _ =  TextIO.closeOut outfile
@@ -165,7 +165,7 @@
                                                    then  
 
                                                  (
-                                                      let    val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                       (* val _ =  OS.Process.sleep(Time.fromSeconds 3 );*)
+                                                      let    val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
                                                              val _ = TextIO.output (outfile, (thisLine))
                                              
                                                              val _ =  TextIO.closeOut outfile
@@ -189,7 +189,7 @@
                                                        TextIO.flushOut toParent;
                                                        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
                                                        (* Attempt to prevent several signals from turning up simultaneously *)
-                                                       OS.Process.sleep(Time.fromSeconds 1);
+                                                       Posix.Process.sleep(Time.fromSeconds 1);
                                                         true  
                                                       end) 
                                                      else if ( thisLine = "SPASS beiseite: Ran out of time.\n" ) 
diff -r 81e9f17823ea -r 8fad4bd4e53c src/HOL/Tools/ATP/recon_transfer_proof.ML
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Apr 20 22:43:52 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Apr 21 10:05:06 2005 +0200
@@ -15,7 +15,7 @@
 (* Versions that include type information *)
  
 fun string_of_thm thm = let val _ = set show_sorts
-                                val str = string_of_thm thm
+                                val str = Display.string_of_thm thm
                                 val no_returns =List.filter not_newline (explode str)
                                 val _ = reset show_sorts
                             in 
@@ -222,9 +222,6 @@
                                             (distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas)))
                                          end
                                         
-fun thmstrings [] str = str
-|   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
-
 fun numclstr (vars, []) str = str
 |   numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
                                in
diff -r 81e9f17823ea -r 8fad4bd4e53c src/HOL/Tools/ATP/watcher.ML
--- a/src/HOL/Tools/ATP/watcher.ML	Wed Apr 20 22:43:52 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML	Thu Apr 21 10:05:06 2005 +0200
@@ -108,7 +108,7 @@
                                        
                                                       in   
                                                          goals_being_watched := (!goals_being_watched) + 1;
-                                                         OS.Process.sleep(Time.fromSeconds 1); 
+                                                         Posix.Process.sleep(Time.fromSeconds 1); 
                      					(warning ("probfile is: "^probfile));
                                                          (warning("dfg file is: "^newfile));
                                                          (warning ("wholefile is: "^(File.sysify_path wholefile)));
@@ -483,7 +483,7 @@
                                                     val parentID = Posix.ProcEnv.getppid()
                                                     val newProcList' =checkChildren (newProcList, toParentStr) 
                                                   in
-                                                    (*OS.Process.sleep (Time.fromSeconds 1);*)
+                                                    (*Posix.Process.sleep (Time.fromSeconds 1);*)
                                                     loop (newProcList') 
                                                   end
                                                   )
@@ -495,7 +495,7 @@
                                                     val parentID = Posix.ProcEnv.getppid()
                                                     val newProcList' =checkChildren (newProcList, toParentStr) 
                                                   in
-                                                    (*OS.Process.sleep (Time.fromSeconds 1);*)
+                                                    (*Posix.Process.sleep (Time.fromSeconds 1);*)
                                                     loop (newProcList') 
                                                   end
                                                   )
@@ -508,7 +508,7 @@
                                                                                           (******************************)
                                         (    let val newProcList = checkChildren ((procList), toParentStr)
                                              in
-                                               OS.Process.sleep (Time.fromSeconds 1);
+                                               Posix.Process.sleep (Time.fromSeconds 1);
                                                loop (newProcList)
                                              end