make SML/NJ and Poly/ML agree on the type of "before";

--- 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";

--- 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;