diff -r 3261ee47bb95 -r f9a20c2c3b70 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Jul 09 13:16:10 2013 +0200
+++ b/src/Pure/System/session.scala	Tue Jul 09 13:17:22 2013 +0200
@@ -396,11 +396,11 @@
               val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
               accumulate(state_id, prover.get.xml_cache.elem(message))
 
-            case Markup.Assign_Execs =>
+            case Markup.Assign_Update =>
               XML.content(output.body) match {
-                case Protocol.Assign(id, assign) =>
+                case Protocol.Assign_Update(id, update) =>
                   try {
-                    val cmds = global_state >>> (_.assign(id, assign))
+                    val cmds = global_state >>> (_.assign(id, update))
                     delay_commands_changed.invoke(true, cmds)
                   }
                   catch { case _: Document.State.Fail => bad_output() }