1.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Feb 04 16:03:15 2010 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Feb 04 16:50:26 2010 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  
     1.5  val defs = Nitpick_HOL.all_axioms_of @{theory} |> #1
     1.6  val def_table = Nitpick_HOL.const_def_table @{context} defs
     1.7 -val ext_ctxt : Nitpick_HOL.extended_context =
     1.8 +val hol_ctxt : Nitpick_HOL.hol_context =
     1.9    {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
    1.10     stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false,
    1.11     binary_ints = SOME false, destroy_constrs = false, specialize = false,
    1.12 @@ -29,7 +29,7 @@
    1.13     special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
    1.14     wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
    1.15  (* term -> bool *)
    1.16 -val is_mono = Nitpick_Mono.formulas_monotonic ext_ctxt @{typ 'a}
    1.17 +val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt @{typ 'a}
    1.18                                                Nitpick_Mono.Plus [] []
    1.19  fun is_const t =
    1.20    let val T = fastype_of t in

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Feb 04 16:03:15 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Feb 04 16:50:26 2010 +0100
     2.3 @@ -431,7 +431,8 @@
     2.4            {delta = 0, epsilon = 1,
     2.5             exclusive = (s = @{const_name Nil} andalso length constrs = 2),
     2.6             total = true}
     2.7 -        else if s = @{const_name Cons} andalso length constrs = 2 then
     2.8 +        else if s = @{const_name Cons} andalso
     2.9 +                num_self_recs + num_non_self_recs = 2 then
    2.10            {delta = 1, epsilon = card, exclusive = true, total = false}
    2.11          else
    2.12            {delta = 0, epsilon = card, exclusive = false, total = false}