--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Thu Jun 01 21:24:33 2017 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Thu Jun 01 21:43:36 2017 +0200
@@ -1790,8 +1790,7 @@
(on_load : proof_annotation -> theory -> (proof_annotation * theory)) thy =
let
val prob_name =
- Path.base file_name
- |> Path.implode
+ Path.base_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