# HG changeset patch
# User blanchet
# Date 1298309308 -3600
# Node ID a96684499e854879a944a13c713e7ce835ad1fb3
# Parent  90dd5291afd81c46d6d2f47b7e788b1e18cb5137
adjust example

diff -r 90dd5291afd8 -r a96684499e85 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Feb 21 18:02:14 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Feb 21 18:28:28 2011 +0100
@@ -38,7 +38,7 @@
   {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [],
    stds = stds, wfs = [], user_axioms = NONE, debug = false,
    whacks = [], binary_ints = SOME false, destroy_constrs = true,
-   specialize = false, star_linear_preds = false,
+   specialize = false, star_linear_preds = false, preconstrs = [],
    tac_timeout = NONE, evals = [], case_names = case_names,
    def_tables = def_tables, nondef_table = nondef_table,
    user_nondefs = user_nondefs, simp_table = simp_table,
@@ -188,7 +188,7 @@
       let
         val t = th |> prop_of |> Type.legacy_freeze |> close_form
         val neg_t = Logic.mk_implies (t, @{prop False})
-        val (nondef_ts, def_ts, _, _, _) =
+        val (nondef_ts, def_ts, _, _, _, _) =
           time_limit preproc_timeout (preprocess_formulas hol_ctxt []) neg_t
         val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
       in File.append path (res ^ "\n"); writeln res end