--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Aug 05 20:17:50 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Aug 05 21:56:22 2010 +0200
@@ -20,9 +20,9 @@
val hol_ctxt : Nitpick_HOL.hol_context =
{thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false,
- binary_ints = SOME false, destroy_constrs = false, specialize = false,
- star_linear_preds = false, fast_descrs = false, tac_timeout = NONE,
- evals = [], case_names = [], def_table = def_table,
+ whacks = [], binary_ints = SOME false, destroy_constrs = false,
+ specialize = false, star_linear_preds = false, fast_descrs = false,
+ tac_timeout = NONE, evals = [], case_names = [], def_table = def_table,
nondef_table = Symtab.empty, user_nondefs = [],
simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty,
choice_spec_table = Symtab.empty, intro_table = Symtab.empty,