diff -r c5b3860d29ef -r b6dacf6eabe3 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Wed Nov 28 16:14:31 2018 +0100
@@ -1790,7 +1790,7 @@
  (on_load : proof_annotation -> theory -> (proof_annotation * theory)) thy =
   let
     val prob_name =
-      Path.base_name file_name
+      Path.file_name file_name
       |> TPTP_Problem_Name.parse_problem_name
     val thy1 = TPTP_Interpret.import_file cautious path_prefixes file_name [] [] thy
     val fms = get_fmlas_of_prob thy1 prob_name