src/Pure/Tools/print_operation.scala

--- a/src/Pure/Tools/print_operation.scala	Fri Nov 06 14:43:05 2015 +0100
+++ b/src/Pure/Tools/print_operation.scala	Fri Nov 06 18:15:35 2015 +0100
@@ -20,7 +20,7 @@
 
   class Handler extends Session.Protocol_Handler
   {
-    private val print_operations = Synchronized(Nil: List[(String, String)])
+    private val print_operations = Synchronized[List[(String, String)]](Nil)
 
     def get: List[(String, String)] = print_operations.value