changeset 71383 | 8313dca6dee9 |
parent 69904 | 6f5bd59f75f4 |
child 71601 | 97ccf48c2f0c |
--- a/src/Pure/General/path.scala Wed Jan 15 19:49:13 2020 +0100 +++ b/src/Pure/General/path.scala Wed Jan 15 19:54:50 2020 +0100 @@ -233,7 +233,7 @@ case x => List(x) } - new Path(Path.norm_elems(elems.map(eval).flatten)) + new Path(Path.norm_elems(elems.flatMap(eval))) } def expand: Path = expand_env(Isabelle_System.settings())