# HG changeset patch
# User blanchet
# Date 1265298626 -3600
# Node ID 3df45b0ce8194d3ea7fd2c6e6b999a7264a6ac88
# Parent  96136eb6218f64d31f1dcec428b17e06118a16a7
adapted example following previous Nitpick change and fixed minor optimization in Nitpick

diff -r 96136eb6218f -r 3df45b0ce819 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Feb 04 16:03:15 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Feb 04 16:50:26 2010 +0100
@@ -16,7 +16,7 @@
 
 val defs = Nitpick_HOL.all_axioms_of @{theory} |> #1
 val def_table = Nitpick_HOL.const_def_table @{context} defs
-val ext_ctxt : Nitpick_HOL.extended_context =
+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,
@@ -29,7 +29,7 @@
    special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
    wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
 (* term -> bool *)
-val is_mono = Nitpick_Mono.formulas_monotonic ext_ctxt @{typ 'a}
+val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt @{typ 'a}
                                               Nitpick_Mono.Plus [] []
 fun is_const t =
   let val T = fastype_of t in
diff -r 96136eb6218f -r 3df45b0ce819 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Feb 04 16:03:15 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Feb 04 16:50:26 2010 +0100
@@ -431,7 +431,8 @@
           {delta = 0, epsilon = 1,
            exclusive = (s = @{const_name Nil} andalso length constrs = 2),
            total = true}
-        else if s = @{const_name Cons} andalso length constrs = 2 then
+        else if s = @{const_name Cons} andalso
+                num_self_recs + num_non_self_recs = 2 then
           {delta = 1, epsilon = card, exclusive = true, total = false}
         else
           {delta = 0, epsilon = card, exclusive = false, total = false}