--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Thu Jun 01 21:24:33 2017 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Thu Jun 01 21:43:36 2017 +0200
@@ -955,15 +955,13 @@
let
val config =
{cautious = cautious,
- problem_name =
- SOME (TPTP_Problem_Name.parse_problem_name ((Path.base #> Path.implode)
- file_name))}
+ problem_name = SOME (TPTP_Problem_Name.parse_problem_name (Path.base_name file_name))}
in interpret_file' config [] path_prefixes file_name end
fun import_file cautious path_prefixes file_name type_map const_map thy =
let
val prob_name =
- TPTP_Problem_Name.parse_problem_name (Path.implode (Path.base file_name))
+ TPTP_Problem_Name.parse_problem_name (Path.base_name file_name)
val (result, thy') =
interpret_file cautious path_prefixes file_name type_map const_map thy
(*FIXME doesn't check if problem has already been interpreted*)