src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy

   |> Path.explode
   |> single
 
 val prob_names =
   probs
-  |> map (Path.base_name #> TPTP_Problem_Name.Nonstandard)
+  |> map (Path.file_name #> TPTP_Problem_Name.Nonstandard)
 \<close>
 
 setup \<open>
   if test_all @{context} then I
   else

   info about the inferences for which reconstruction failed.*)
 fun test_partial_reconstruction thy prob_file =
   let
     val prob_name =
       prob_file
-      |> Path.base_name
+      |> Path.file_name
       |> TPTP_Problem_Name.Nonstandard
 
     val thy' =
       try
        (TPTP_Reconstruct.import_thm

          file leo2_on_load thy
 
       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))
        (fn prob_name =>
         (can