--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Mon Mar 03 22:33:22 2014 +0100
@@ -71,7 +71,7 @@
("verbose", "false"),
("overlord", "false"),
("spy", "false"),
- ("show_datatypes", "false"),
+ ("show_types", "false"),
("show_skolems", "true"),
("show_consts", "false"),
("format", "1"),
@@ -100,7 +100,7 @@
("quiet", "verbose"),
("no_overlord", "overlord"),
("dont_spy", "spy"),
- ("hide_datatypes", "show_datatypes"),
+ ("hide_types", "show_types"),
("hide_skolems", "show_skolems"),
("hide_consts", "show_consts"),
("trust_potential", "check_potential"),
@@ -125,6 +125,7 @@
else if String.isPrefix "non_" name then SOME (unprefix "non_" name)
else NONE
| some_name => some_name
+
fun normalize_raw_param (name, value) =
case unnegate_param_name name of
SOME name' => [(name', case value of
@@ -133,7 +134,7 @@
| [] => ["false"]
| _ => value)]
| NONE => if name = "show_all" then
- [("show_datatypes", value), ("show_skolems", value),
+ [("show_types", value), ("show_skolems", value),
("show_consts", value)]
else
[(name, value)]
@@ -267,7 +268,7 @@
val tac_timeout = lookup_time "tac_timeout"
val max_threads =
if mode = Normal then Int.max (0, lookup_int "max_threads") else 1
- val show_datatypes = debug orelse lookup_bool "show_datatypes"
+ val show_types = debug orelse lookup_bool "show_types"
val show_skolems = debug orelse lookup_bool "show_skolems"
val show_consts = debug orelse lookup_bool "show_consts"
val evals = lookup_term_list_option_polymorphic "eval" |> these
@@ -297,7 +298,7 @@
datatype_sym_break = datatype_sym_break,
kodkod_sym_break = kodkod_sym_break, timeout = timeout,
tac_timeout = tac_timeout, max_threads = max_threads,
- show_datatypes = show_datatypes, show_skolems = show_skolems,
+ show_types = show_types, show_skolems = show_skolems,
show_consts = show_consts, evals = evals, formats = formats,
atomss = atomss, max_potential = max_potential, max_genuine = max_genuine,
check_potential = check_potential, check_genuine = check_genuine,