diff --git a/src/HOL/Tools/ATP/system_on_tptp.ML b/src/HOL/Tools/ATP/system_on_tptp.ML
--- a/src/HOL/Tools/ATP/system_on_tptp.ML
+++ b/src/HOL/Tools/ATP/system_on_tptp.ML
@@ -1,20 +1,24 @@
 (*  Title:      HOL/Tools/ATP/system_on_tptp.ML
     Author:     Makarius
 
 Support for remote ATPs via SystemOnTPTP.
 *)
 
 signature SYSTEM_ON_TPTP =
 sig
   val get_url: unit -> string
-  val list_systems: unit -> string list
+  val list_systems: unit -> {url: string, systems: string list}
 end
 
 structure SystemOnTPTP: SYSTEM_ON_TPTP =
 struct
 
 fun get_url () = Options.default_string \<^system_option>\<open>SystemOnTPTP\<close>
 
-fun list_systems () = get_url () |> \<^scala>\<open>SystemOnTPTP.list_systems\<close> |> split_lines
+fun list_systems () =
+  let
+    val url = get_url ()
+    val systems = split_lines (\<^scala>\<open>SystemOnTPTP.list_systems\<close> url)
+  in {url = url, systems = systems} end
 
 end