tuned;

--- a/src/Pure/General/path.scala	Wed Sep 14 12:12:44 2016 +0200
+++ b/src/Pure/General/path.scala	Wed Sep 14 12:51:40 2016 +0200
@@ -96,7 +96,7 @@
       else (List(root_elem(es.head)), es.tail)
     val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem)
 
-    new Path(norm_elems(elems.reverse ::: roots))
+    new Path(norm_elems(elems reverse_::: roots))
   }
 
   def is_wellformed(str: String): Boolean =

--- a/src/Pure/Thy/thy_syntax.scala	Wed Sep 14 12:12:44 2016 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Sep 14 12:51:40 2016 +0200
@@ -198,7 +198,7 @@
     val removed = old_cmds.iterator.filter(!new_cmds.contains(_)).toList
     val inserted = new_cmds.iterator.filter(!old_cmds.contains(_)).toList
 
-    removed.reverse.map(cmd => (old_cmds.prev(cmd), None)) :::
+    removed.map(cmd => (old_cmds.prev(cmd), None)) reverse_:::
     inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd)))
   }