discontinued odd workaround for some old Poly/ML, which is still supported but of little practical relevance;
authorwenzelm
Wed Jul 03 21:38:10 2013 +0200 (2013-07-03 ago)
changeset 5251304210c1bcb90
parent 52512 c4891dbd5161
child 52514 8dd8ab81f1d7
discontinued odd workaround for some old Poly/ML, which is still supported but of little practical relevance;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Jul 03 21:32:58 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Jul 03 21:38:10 2013 +0200
     1.3 @@ -472,7 +472,6 @@
     1.4  fun update (old_id: version_id) (new_id: version_id) edits state =
     1.5    let
     1.6      val old_version = the_version state old_id;
     1.7 -    val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
     1.8      val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version);
     1.9  
    1.10      val nodes = nodes_of new_version;