# HG changeset patch
# User blanchet
# Date 1281038182 -7200
# Node ID 7f4755c5e77b89d4e170c988a2341477a668696b
# Parent  3d1d928dce503f81d87619c44b84e44b82de6775
added record field

diff -r 3d1d928dce50 -r 7f4755c5e77b src/HOL/Nitpick_Examples/Mono_Nits.thy
--- 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,