--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 14 12:52:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 14 13:24:18 2010 +0200
@@ -34,7 +34,6 @@
destroy_constrs: bool,
specialize: bool,
star_linear_preds: bool,
- fast_descrs: bool,
peephole_optim: bool,
datatype_sym_break: int,
kodkod_sym_break: int,
@@ -108,7 +107,6 @@
destroy_constrs: bool,
specialize: bool,
star_linear_preds: bool,
- fast_descrs: bool,
peephole_optim: bool,
datatype_sym_break: int,
kodkod_sym_break: int,
@@ -207,10 +205,10 @@
boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
verbose, overlord, user_axioms, assms, whacks, merge_type_vars,
binary_ints, destroy_constrs, specialize, star_linear_preds,
- fast_descrs, peephole_optim, datatype_sym_break, kodkod_sym_break,
- tac_timeout, max_threads, show_datatypes, show_consts, evals, formats,
- atomss, max_potential, max_genuine, check_potential, check_genuine,
- batch_size, ...} = params
+ peephole_optim, datatype_sym_break, kodkod_sym_break, tac_timeout,
+ max_threads, show_datatypes, show_consts, evals, formats, atomss,
+ max_potential, max_genuine, check_potential, check_genuine, batch_size,
+ ...} = params
val state_ref = Unsynchronized.ref state
val pprint =
if auto then
@@ -280,14 +278,13 @@
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
whacks = whacks, binary_ints = binary_ints,
destroy_constrs = destroy_constrs, specialize = specialize,
- star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
- tac_timeout = tac_timeout, evals = evals, case_names = case_names,
- def_table = def_table, nondef_table = nondef_table,
- user_nondefs = user_nondefs, simp_table = simp_table,
- psimp_table = psimp_table, choice_spec_table = choice_spec_table,
- intro_table = intro_table, ground_thm_table = ground_thm_table,
- ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
- special_funs = Unsynchronized.ref [],
+ star_linear_preds = star_linear_preds, tac_timeout = tac_timeout,
+ evals = evals, case_names = case_names, def_table = def_table,
+ nondef_table = nondef_table, user_nondefs = user_nondefs,
+ simp_table = simp_table, psimp_table = psimp_table,
+ choice_spec_table = choice_spec_table, intro_table = intro_table,
+ ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
+ skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
constr_cache = Unsynchronized.ref []}
val pseudo_frees = fold Term.add_frees assm_ts []