--- 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