src/Pure/PIDE/document.ML

--- a/src/Pure/PIDE/document.ML	Thu Jul 11 16:01:48 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Jul 11 16:26:14 2013 +0200
@@ -334,7 +334,7 @@
                 (fn () =>
                   iterate_entries (fn (_, opt_exec) => fn () =>
                     (case opt_exec of
-                      SOME exec => if running () then SOME (Command.execute exec) else NONE
+                      SOME exec => if running () then SOME (Command.exec exec) else NONE
                     | NONE => NONE)) node ()));
   in () end;