tuned;

--- a/src/Pure/General/file.scala	Sun Feb 28 14:33:53 2016 +0100
+++ b/src/Pure/General/file.scala	Sun Feb 28 14:48:38 2016 +0100
@@ -196,13 +196,13 @@
   def write_backup(path: Path, text: CharSequence)
   {
     path.file renameTo path.backup.file
-    File.write(path, text)
+    write(path, text)
   }
 
   def write_backup2(path: Path, text: CharSequence)
   {
     path.file renameTo path.backup2.file
-    File.write(path, text)
+    write(path, text)
   }