# HG changeset patch
# User wenzelm
# Date 924798324 -7200
# Node ID 7954ffeb93f3c1e3fe94d9cabf5229c444eb9297
# Parent  4961ecbaaff7623a35a75d46ab83d55c40fe847b
fixed IO;

diff -r 4961ecbaaff7 -r 7954ffeb93f3 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Thu Apr 22 18:25:07 1999 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Thu Apr 22 18:25:24 1999 +0200
@@ -492,14 +492,12 @@
 (setmp print_mode ["Mucke"] (make_string sign) terms)
 end;
 
-fun callmc s = 
-let 
-val a = TextIO.openOut("tmp.mu");
-val _ = output(a,s);
-val _ = TextIO.closeOut(a);
-in
-execute("mucke -nb tmp")
-end; 
+fun callmc s =
+  let
+    val path = Path.unpack "tmp.mu";
+    val _ = File.write path s;
+    val result = execute "mucke -nb tmp";
+  in File.rm path; result end;
 
 (* extract_result looks for true value before *) 
 (* finishing line "===..." of mucke output    *)