--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Feb 26 20:40:45 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Feb 28 17:53:10 2011 +0100
@@ -58,6 +58,7 @@
("destroy_constrs", "true"),
("specialize", "true"),
("star_linear_preds", "true"),
+ ("total_consts", "smart"),
("preconstr", "smart"),
("peephole_optim", "true"),
("datatype_sym_break", "5"),
@@ -91,6 +92,7 @@
("dont_destroy_constrs", "destroy_constrs"),
("dont_specialize", "specialize"),
("dont_star_linear_preds", "star_linear_preds"),
+ ("partial_consts", "total_consts"),
("dont_preconstr", "preconstr"),
("no_peephole_optim", "peephole_optim"),
("no_debug", "debug"),
@@ -253,6 +255,7 @@
val destroy_constrs = lookup_bool "destroy_constrs"
val specialize = lookup_bool "specialize"
val star_linear_preds = lookup_bool "star_linear_preds"
+ val total_consts = lookup_bool_option "total_consts"
val preconstrs =
lookup_bool_option_assigns read_term_polymorphic "preconstr"
val peephole_optim = lookup_bool "peephole_optim"
@@ -285,8 +288,9 @@
user_axioms = user_axioms, assms = assms, whacks = whacks,
merge_type_vars = merge_type_vars, binary_ints = binary_ints,
destroy_constrs = destroy_constrs, specialize = specialize,
- star_linear_preds = star_linear_preds, preconstrs = preconstrs,
- peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break,
+ star_linear_preds = star_linear_preds, total_consts = total_consts,
+ preconstrs = preconstrs, peephole_optim = peephole_optim,
+ 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_consts = show_consts,