changeset 58893 | 9e0ecb66d6a7 |
parent 57808 | cf72aed038c8 |
child 59936 | b8ffc3dc9e24 |
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Mon Nov 03 14:31:15 2014 +0100 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Mon Nov 03 14:50:27 2014 +0100 @@ -912,7 +912,7 @@ in TPTP_Data.map (cons ((prob_name, result))) thy' end val _ = - Outer_Syntax.improper_command @{command_spec "import_tptp"} "import TPTP problem" + Outer_Syntax.command @{command_spec "import_tptp"} "import TPTP problem" (Parse.path >> (fn name => Toplevel.theory (fn thy => let val path = Path.explode name