src/Pure/library.scala

--- a/src/Pure/library.scala	Mon May 22 15:19:44 2017 +0200
+++ b/src/Pure/library.scala	Mon May 22 19:34:01 2017 +0200
@@ -142,7 +142,7 @@
   def trim_split_lines(s: String): List[String] =
     split_lines(trim_line(s)).map(trim_line(_))
 
-  def trim_substring(s: String): String = new String(s.toCharArray)
+  def isolate_substring(s: String): String = new String(s.toCharArray)
 
 
   /* quote */