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