# HG changeset patch
# User wenzelm
# Date 1473850300 -7200
# Node ID 630eaf8fe9f3cda4f535be4ee922d93b7324a1ec
# Parent  ccac33e291b1243fba3bee865f4beb004915c65f
tuned;

diff -r ccac33e291b1 -r 630eaf8fe9f3 src/Pure/General/path.scala
--- 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 =
diff -r ccac33e291b1 -r 630eaf8fe9f3 src/Pure/Thy/thy_syntax.scala
--- 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)))
   }