--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Thu Mar 15 22:08:53 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Thu Mar 15 22:20:07 2012 +0100
@@ -887,14 +887,9 @@
in TPTP_Data.map (cons ((prob_name, result))) thy' end
val _ =
- Outer_Syntax.improper_command "import_tptp" "import TPTP problem"
- Keyword.diag (*FIXME why diag?*)
- (Parse.string >>
- (fn file_name =>
- Toplevel.theory (fn thy =>
- import_file true (Path.explode file_name |> Path.dir)
- (Path.explode file_name) [] [] thy
- )))
+ Outer_Syntax.improper_command "import_tptp" "import TPTP problem" Keyword.thy_decl
+ (Parse.path >> (fn path =>
+ Toplevel.theory (fn thy => import_file true (Path.dir path) path [] [] thy)))
(*Used for debugging. Returns all files contained within a directory or its