diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/library.scala
--- a/src/Pure/library.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/library.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -140,7 +140,7 @@
     else s
 
   def trim_split_lines(s: String): List[String] =
-    split_lines(trim_line(s)).map(trim_line(_))
+    split_lines(trim_line(s)).map(trim_line)
 
   def isolate_substring(s: String): String = new String(s.toCharArray)
 
@@ -204,7 +204,7 @@
   def is_regex_meta(c: Char): Boolean = """()[]{}\^$|?*+.<>-=!""".contains(c)
 
   def escape_regex(s: String): String =
-    if (s.exists(is_regex_meta(_))) {
+    if (s.exists(is_regex_meta)) {
       (for (c <- s.iterator)
        yield { if (is_regex_meta(c)) "\\" + c.toString else c.toString }).mkString
     }