1.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Sep 13 20:15:04 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Sep 13 20:21:24 2010 +0200
     1.3 @@ -26,6 +26,10 @@
     1.4  
     1.5  val auto = Unsynchronized.ref false
     1.6  
     1.7 +(* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share
     1.8 +   its time slot with several other automatic tools. *)
     1.9 +val max_auto_scopes = 6
    1.10 +
    1.11  val _ =
    1.12    ProofGeneralPgip.add_preference Preferences.category_tracing
    1.13        (Preferences.bool_pref auto "auto-nitpick"
    1.14 @@ -223,6 +227,7 @@
    1.15        AList.lookup (op =) raw_params #> these #> map read_term_polymorphic
    1.16      val read_const_polymorphic = read_term_polymorphic #> dest_Const
    1.17      val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1
    1.18 +                        |> auto ? map (apsnd (take max_auto_scopes))
    1.19      val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1
    1.20      val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
    1.21      val bitss = lookup_int_seq "bits" 1