src/HOL/TPTP/atp_problem_import.ML

-(*  Title:      HOL/TPTP/atp_problem_import.ML
+Nitpick_Commands(*  Title:      HOL/TPTP/atp_problem_import.ML
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2012
 
 Import TPTP problems as Isabelle terms or goals.
 *)

        ("show_consts", "true"),
        ("format", "1"),
        ("max_potential", "0"),
        ("timeout", string_of_int timeout),
        ("tac_timeout", string_of_int ((timeout + 49) div 50))]
-      |> Nitpick_Isar.default_params thy
+      |> Nitpick_Commands.default_params thy
     val i = 1
     val n = 1
     val step = 0
     val subst = []
   in

            ("verbose", "true"),
            ("debug", if debug then "true" else "false"),
            ("overlord", if overlord then "true" else "false"),
            ("max_potential", "0"),
            ("timeout", string_of_int timeout)]
-          |> Nitpick_Isar.default_params thy
+          |> Nitpick_Commands.default_params thy
         val i = 1
         val n = 1
         val step = 0
         val subst = []
         val (outcome, _) =