# HG changeset patch
# User wenzelm
# Date 1375104002 -7200
# Node ID 5009911c7403be6a8b25dcc2172035ea0331ba27
# Parent  8c7cf864e270a2816791e96ffefb691861b52ca8
tuned;

diff -r 8c7cf864e270 -r 5009911c7403 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Jul 29 15:09:20 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Jul 29 15:20:02 2013 +0200
@@ -199,7 +199,7 @@
 type execution = {version_id: Document_ID.version, execution_id: Document_ID.execution};
 
 val no_execution = {version_id = Document_ID.none, execution_id = Document_ID.none};
-fun next_execution version_id = {version_id = version_id, execution_id = Execution.start ()};
+fun new_execution version_id = {version_id = version_id, execution_id = Execution.start ()};
 
 abstype state = State of
  {versions: version Inttab.table,  (*version id -> document content*)
@@ -226,7 +226,7 @@
     let
       val versions' = Inttab.update_new (version_id, version) versions
         handle Inttab.DUP dup => err_dup "document version" dup;
-      val execution' = next_execution version_id;
+      val execution' = new_execution version_id;
     in (versions', commands, execution') end);
 
 fun the_version (State {versions, ...}) version_id =