# HG changeset patch # User wenzelm # Date 1372880290 -7200 # Node ID 04210c1bcb90f3ff0c381097d76969f17f217835 # Parent c4891dbd51614e38bf3dbec5ebd0aa6b57152e9c discontinued odd workaround for some old Poly/ML, which is still supported but of little practical relevance; diff -r c4891dbd5161 -r 04210c1bcb90 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Wed Jul 03 21:32:58 2013 +0200 +++ b/src/Pure/PIDE/document.ML Wed Jul 03 21:38:10 2013 +0200 @@ -472,7 +472,6 @@ fun update (old_id: version_id) (new_id: version_id) edits state = let val old_version = the_version state old_id; - val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 *) val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version); val nodes = nodes_of new_version;