# HG changeset patch
# User blanchet
# Date 1258498077 -3600
# Node ID 3aa6b991125203103f09c10cfe4d8b3641c9afb4
# Parent  6c6ce0757bfef2256782d7d954d2522c10392639
bump up Nitpick's axiom/definition unfolding limits, because some real-world problems (e.g. from Boogie) ran into the previous limits;
the limits are there to prevent infinite recursion; they can be set arbitrarily high without much harm

diff -r 6c6ce0757bfe -r 3aa6b9911252 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Tue Nov 17 22:51:00 2009 +0100
+++ b/src/HOL/Nitpick.thy	Tue Nov 17 23:47:57 2009 +0100
@@ -213,7 +213,7 @@
 (* While Nitpick normally avoids to unfold definitions for locales, it
    unfortunately needs to unfold them when dealing with the following built-in
    constants. A cleaner approach would be to change "Nitpick_HOL" and
-   "Nitpick_Nits" so that they handle the unexpanded overloaded constants
+   "Nitpick_Nut" so that they handle the unexpanded overloaded constants
    directly, but this is slightly more tricky to implement. *)
 lemmas [nitpick_def] = div_int_inst.div_int div_int_inst.mod_int
     div_nat_inst.div_nat div_nat_inst.mod_nat lower_semilattice_fun_inst.inf_fun
diff -r 6c6ce0757bfe -r 3aa6b9911252 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 17 22:51:00 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 17 23:47:57 2009 +0100
@@ -1416,8 +1416,8 @@
     SOME t' => is_constr_pattern_lhs thy t'
   | NONE => false
 
-val unfold_max_depth = 63
-val axioms_max_depth = 63
+val unfold_max_depth = 255
+val axioms_max_depth = 255
 
 (* extended_context -> term -> term *)
 fun unfold_defs_in_term (ext_ctxt as {thy, destroy_constrs, fast_descrs,