src/HOL/TPTP/atp_problem_import.ML
changeset 55199 ba93ef2c0d27
parent 54547 c999e2533487
child 55201 1ee776da8da7
--- a/src/HOL/TPTP/atp_problem_import.ML	Fri Jan 31 10:23:32 2014 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Jan 31 10:23:32 2014 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/TPTP/atp_problem_import.ML
+Nitpick_Commands(*  Title:      HOL/TPTP/atp_problem_import.ML
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2012
 
@@ -93,7 +93,7 @@
        ("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
@@ -168,7 +168,7 @@
            ("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