src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML

       in TPTP_Reconstruction_Data.map (cons ((prob_name, pannot))) thy5 end
   end
 
 (*This has been disabled since it requires a hook to be specified to use "import_thm"
 val _ =
-  Outer_Syntax.improper_command @{command_spec "import_leo2_proof"} "import TPTP proof"
+  Outer_Syntax.command @{command_spec "import_leo2_proof"} "import TPTP proof"
     (Parse.path >> (fn name =>
       Toplevel.theory (fn thy =>
        let val path = Path.explode name
        in import_thm true [Path.dir path, Path.explode "$TPTP"] path (*FIXME hook needs to be given here*)
 thy end)))