--- a/src/HOL/Tools/ATP/system_on_tptp.scala Sat Mar 13 14:27:34 2021 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala Sat Mar 13 14:55:27 2021 +0100
@@ -35,11 +35,8 @@
/* list systems */
- def proper_lines(content: HTTP.Content): List[String] =
- Library.trim_split_lines(content.text).filterNot(_.startsWith("%"))
-
def list_systems(url: URL): List[String] =
- proper_lines(post_request(url, List("SubmitButton" -> "ListSystems", "ListStatus" -> "READY")))
+ post_request(url, List("SubmitButton" -> "ListSystems", "ListStatus" -> "READY")).text_lines
object List_Systems extends Scala.Fun("SystemOnTPTP.list_systems", thread = true)
{