# HG changeset patch
# User wenzelm
# Date 934904058 -7200
# Node ID 6e7b6b8490e0649faa432528b7b50645590a118d
# Parent  830d7d52059292d6c657280561397ab2c052be7a
remove tmp files;

diff -r 830d7d520592 -r 6e7b6b8490e0 src/HOL/Tools/svc_funcs.ML
--- a/src/HOL/Tools/svc_funcs.ML	Tue Aug 17 17:33:47 1999 +0200
+++ b/src/HOL/Tools/svc_funcs.ML	Tue Aug 17 17:34:18 1999 +0200
@@ -90,8 +90,9 @@
 			"> /dev/null 2>&1"))
       val svc_output = File.read svc_output_file
 	               handle _ => error "SVC returned no output"
-      val _ = if !trace then writeln ("SVC Returns:\n" ^ svc_output) else ()
   in
+      if ! trace then writeln ("SVC Returns:\n" ^ svc_output) else ();
+      if not (! trace) then (File.rm svc_input_file; File.rm svc_output_file) else ();
       String.isPrefix "VALID" svc_output
   end