# HG changeset patch
# User wenzelm
# Date 1292928875 -3600
# Node ID 87adb55fb0fb12443e719d4134eb91ca4ecaf238
# Parent  e82fc600a3a5df39fdb7ca1231dc61f15329c149
make SML/NJ and Poly/ML agree on the type of "before";

diff -r e82fc600a3a5 -r 87adb55fb0fb src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Tue Dec 21 10:20:33 2010 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Tue Dec 21 11:54:35 2010 +0100
@@ -3,6 +3,8 @@
 Compatibility file for Poly/ML -- common part for 5.x.
 *)
 
+fun op before (a, _: unit) = a;
+
 exception Interrupt = SML90.Interrupt;
 
 use "General/exn.ML";
diff -r e82fc600a3a5 -r 87adb55fb0fb src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Tue Dec 21 10:20:33 2010 +0100
+++ b/src/Pure/System/isabelle_system.ML	Tue Dec 21 11:54:35 2010 +0100
@@ -65,13 +65,13 @@
 
 fun with_tmp_file name f =
   let val path = fresh_path name
-  in Exn.release (Exn.capture f path before try File.rm path) end;
+  in Exn.release (Exn.capture f path before ignore (try File.rm path)) end;
 
 fun with_tmp_dir name f =
   let
     val path = fresh_path name;
     val _ = mkdirs path;
-  in Exn.release (Exn.capture f path before try rm_tree path) end;
+  in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end;
 
 end;