src/Pure/ML-Systems/smlnj.ML
changeset 40748 591b6778d076
parent 40627 becf5d5187cc
child 41411 3bcc3b9e1020
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Sat Nov 27 16:27:52 2010 +0100
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Sat Nov 27 16:29:53 2010 +0100
     1.3 @@ -14,7 +14,6 @@
     1.4  use "ML-Systems/thread_dummy.ML";
     1.5  use "ML-Systems/multithreading.ML";
     1.6  use "General/timing.ML";
     1.7 -use "ML-Systems/bash.ML";
     1.8  use "ML-Systems/ml_name_space.ML";
     1.9  use "ML-Systems/ml_pretty.ML";
    1.10  structure PolyML = struct end;
    1.11 @@ -170,11 +169,6 @@
    1.12  val pwd = OS.FileSys.getDir;
    1.13  
    1.14  
    1.15 -(* system command execution *)
    1.16 -
    1.17 -val bash_output = (fn (output, rc) => (output, mk_int rc)) o bash_output;
    1.18 -
    1.19 -
    1.20  (* getenv *)
    1.21  
    1.22  fun getenv var =