1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Wed Apr 19 10:43:09 2006 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Wed Apr 19 10:43:53 2006 +0200
     1.3 @@ -195,12 +195,16 @@
     1.4               error "")
     1.5      | numbers => valOf (Int.fromString (List.last numbers));
     1.6  
     1.7 -(* call ATP.  Settings should be a list of strings  ["-t300", "-m100000"]*)
     1.8 +(*Call ATP.  Settings should be a list of strings  ["-t 300", "-m 100000"],
     1.9 +  which we convert below to ["-t", "300", "-m", "100000"] using String.tokens.
    1.10 +  Otherwise, the SML/NJ version of Unix.execute will escape the spaces, and
    1.11 +  Vampire will reject the switches.*)
    1.12  fun execCmds [] procList = procList
    1.13    | execCmds ((prover,proverCmd,settings,file)::cmds) procList  =
    1.14        let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ file)
    1.15 +          val settings' = List.concat (map (String.tokens Char.isSpace) settings)
    1.16  	  val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
    1.17 -	       Unix.execute(proverCmd, settings@[file])
    1.18 +	       Unix.execute(proverCmd, settings' @ [file])
    1.19  	  val (instr, outstr) = Unix.streamsOf childhandle
    1.20  	  val newProcList = {prover=prover, file=file, proc_handle=childhandle,
    1.21  			     instr=instr, outstr=outstr} :: procList