src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy

--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Wed Nov 28 16:14:31 2018 +0100
@@ -58,7 +58,7 @@
 
 val prob_names =
   probs
-  |> map (Path.base_name #> TPTP_Problem_Name.Nonstandard)
+  |> map (Path.file_name #> TPTP_Problem_Name.Nonstandard)
 \<close>
 
 setup \<open>
@@ -576,7 +576,7 @@
   let
     val prob_name =
       prob_file
-      |> Path.base_name
+      |> Path.file_name
       |> TPTP_Problem_Name.Nonstandard
 
     val thy' =
@@ -660,7 +660,7 @@
       val ctxt = Proof_Context.init_global thy' (*FIXME pass ctxt instead of thy*)
       val prob_name =
         file
-        |> Path.base_name
+        |> Path.file_name
         |> TPTP_Problem_Name.Nonstandard
     in
       Timeout.apply (Time.fromSeconds (if timeout = 0 then 60 else timeout))