src/HOL/Modelcheck/mucke_oracle.ML
changeset 16258 f3d913abf7e5
parent 16152 7294283b0c45
child 16429 e871f4b1a4f0
     1.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Sun Jun 05 11:31:20 2005 +0200
     1.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Sun Jun 05 11:31:21 2005 +0200
     1.3 @@ -503,7 +503,7 @@
     1.4        else mucke_home ^ "/mucke";
     1.5      val mucke_input_file = File.tmp_path (Path.basic "tmp.mu");
     1.6      val _ = File.write mucke_input_file s;
     1.7 -    val result = execute (mucke ^ " -nb -res " ^ (File.quote_sysify_path mucke_input_file));
     1.8 +    val result = execute (mucke ^ " -nb -res " ^ File.shell_path mucke_input_file);
     1.9    in
    1.10      if not (!trace_mc) then (File.rm mucke_input_file) else (); 
    1.11      result