# HG changeset patch
# User wenzelm
# Date 1615642054 -3600
# Node ID 2b657a70116cd0fcd80cfd6234787ae0b20effac
# Parent  53cba4441cfbe5b5c6248eb7d03308ba7b3ad4f3
clarified signature: url may change dynamically and is part of result;

diff -r 53cba4441cfb -r 2b657a70116c src/HOL/Tools/ATP/system_on_tptp.ML
--- a/src/HOL/Tools/ATP/system_on_tptp.ML	Sat Mar 13 14:27:07 2021 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.ML	Sat Mar 13 14:27:34 2021 +0100
@@ -7,7 +7,7 @@
 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 =
@@ -15,6 +15,10 @@
 
 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