added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Nov 05 17:00:28 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Nov 05 17:03:22 2009 +0100
@@ -263,7 +263,8 @@
        intro_table = intro_table, ground_thm_table = ground_thm_table,
        ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
        special_funs = Unsynchronized.ref [],
-       unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref []}
+       unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
+       constr_cache = Unsynchronized.ref []}
     val frees = Term.add_frees assms_t []
     val _ = null (Term.add_tvars assms_t [])
             orelse raise NOT_SUPPORTED "schematic type variables"
@@ -818,9 +819,19 @@
           run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
         end
 
-    val _ = scopes := all_scopes ext_ctxt sym_break cards_assigns maxes_assigns
-                                 iters_assigns bisim_depths mono_Ts nonmono_Ts
-                                 shallow_dataTs
+    val (skipped, the_scopes) =
+      all_scopes ext_ctxt sym_break cards_assigns maxes_assigns iters_assigns
+                 bisim_depths mono_Ts nonmono_Ts shallow_dataTs
+    val _ = if skipped > 0 then
+              print_m (fn () => "Too many scopes. Dropping " ^
+                                string_of_int skipped ^ " scope" ^
+                                plural_s skipped ^
+                                ". (Consider using \"mono\" or \
+                                \\"merge_type_vars\" to prevent this.)")
+            else
+              ()
+    val _ = scopes := the_scopes
+
     val batches = batch_list batch_size (!scopes)
     val outcome_code =
       (run_batches 0 (length batches) batches (max_potential, max_genuine, 0)

--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Nov 05 17:00:28 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Nov 05 17:03:22 2009 +0100
@@ -40,7 +40,8 @@
     skolems: (string * string list) list Unsynchronized.ref,
     special_funs: special_fun list Unsynchronized.ref,
     unrolled_preds: unrolled list Unsynchronized.ref,
-    wf_cache: wf_cache Unsynchronized.ref}
+    wf_cache: wf_cache Unsynchronized.ref,
+    constr_cache: (typ * styp list) list Unsynchronized.ref}
 
   val name_sep : string
   val numeral_prefix : string
@@ -100,16 +101,16 @@
   val unregister_frac_type : string -> theory -> theory
   val register_codatatype : typ -> string -> styp list -> theory -> theory
   val unregister_codatatype : typ -> theory -> theory
-  val datatype_constrs : theory -> typ -> styp list
+  val datatype_constrs : extended_context -> typ -> styp list
   val boxed_datatype_constrs : extended_context -> typ -> styp list
-  val num_datatype_constrs : theory -> typ -> int
+  val num_datatype_constrs : extended_context -> typ -> int
   val constr_name_for_sel_like : string -> string
   val boxed_constr_for_sel : extended_context -> styp -> styp
   val card_of_type : (typ * int) list -> typ -> int
   val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
   val bounded_precise_card_of_type :
-    theory -> int -> int -> (typ * int) list -> typ -> int
-  val is_finite_type : theory -> typ -> bool
+    extended_context -> int -> int -> (typ * int) list -> typ -> int
+  val is_finite_type : extended_context -> typ -> bool
   val all_axioms_of : theory -> term list * term list * term list
   val arity_of_built_in_const : bool -> styp -> int option
   val is_built_in_const : bool -> styp -> bool
@@ -177,7 +178,8 @@
   skolems: (string * string list) list Unsynchronized.ref,
   special_funs: special_fun list Unsynchronized.ref,
   unrolled_preds: unrolled list Unsynchronized.ref,
-  wf_cache: wf_cache Unsynchronized.ref}
+  wf_cache: wf_cache Unsynchronized.ref,
+  constr_cache: (typ * styp list) list Unsynchronized.ref}
 
 structure TheoryData = TheoryDataFun(
   type T = {frac_types: (string * (string * string) list) list,
@@ -727,7 +729,7 @@
 fun suc_const T = Const (@{const_name Suc}, T --> T)
 
 (* theory -> typ -> styp list *)
-fun datatype_constrs thy (T as Type (s, Ts)) =
+fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
     if is_datatype thy T then
       case Datatype.get_info thy s of
         SOME {index, descr, ...} =>
@@ -757,11 +759,19 @@
               []
     else
       []
-  | datatype_constrs _ _ = []
+  | uncached_datatype_constrs _ _ = []
 (* extended_context -> typ -> styp list *)
-fun boxed_datatype_constrs (ext_ctxt as {thy, ...}) =
-  map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs thy
-(* theory -> typ -> int *)
+fun datatype_constrs (ext_ctxt as {thy, constr_cache, ...} : extended_context)
+                     T =
+  case AList.lookup (op =) (!constr_cache) T of
+    SOME xs => xs
+  | NONE =>
+    let val xs = uncached_datatype_constrs thy T in
+      (Unsynchronized.change constr_cache (cons (T, xs)); xs)
+    end
+fun boxed_datatype_constrs ext_ctxt =
+  map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs ext_ctxt
+(* extended_context -> typ -> int *)
 val num_datatype_constrs = length oo datatype_constrs
 
 (* string -> string *)
@@ -774,26 +784,26 @@
     AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s
     |> the |> pair s
   end
-(* theory -> styp -> term *)
-fun discr_term_for_constr thy (x as (s, T)) =
+(* extended_context -> styp -> term *)
+fun discr_term_for_constr ext_ctxt (x as (s, T)) =
   let val dataT = body_type T in
     if s = @{const_name Suc} then
       Abs (Name.uu, dataT,
            @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
-    else if num_datatype_constrs thy dataT >= 2 then
+    else if num_datatype_constrs ext_ctxt dataT >= 2 then
       Const (discr_for_constr x)
     else
       Abs (Name.uu, dataT, @{const True})
   end
 
-(* theory -> styp -> term -> term *)
-fun discriminate_value thy (x as (_, T)) t =
+(* extended_context -> styp -> term -> term *)
+fun discriminate_value (ext_ctxt as {thy, ...}) (x as (_, T)) t =
   case strip_comb t of
     (Const x', args) =>
     if x = x' then @{const True}
     else if is_constr_like thy x' then @{const False}
-    else betapply (discr_term_for_constr thy x, t)
-  | _ => betapply (discr_term_for_constr thy x, t)
+    else betapply (discr_term_for_constr ext_ctxt x, t)
+  | _ => betapply (discr_term_for_constr ext_ctxt x, t)
 
 (* styp -> term -> term *)
 fun nth_arg_sel_term_for_constr (x as (s, T)) n =
@@ -842,8 +852,8 @@
       | _ => list_comb (Const x, args)
     end
 
-(* theory -> typ -> term -> term *)
-fun constr_expand thy T t =
+(* extended_context -> typ -> term -> term *)
+fun constr_expand (ext_ctxt as {thy, ...}) T t =
   (case head_of t of
      Const x => if is_constr_like thy x then t else raise SAME ()
    | _ => raise SAME ())
@@ -855,7 +865,7 @@
                  (@{const_name Pair}, [T1, T2] ---> T)
                end
              else
-               datatype_constrs thy T |> the_single
+               datatype_constrs ext_ctxt T |> the_single
            val arg_Ts = binder_types T'
          in
            list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
@@ -897,8 +907,8 @@
                     card_of_type asgns T
                     handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
                            default_card)
-(* theory -> int -> (typ * int) list -> typ -> int *)
-fun bounded_precise_card_of_type thy max default_card asgns T =
+(* extended_context -> int -> (typ * int) list -> typ -> int *)
+fun bounded_precise_card_of_type ext_ctxt max default_card asgns T =
   let
     (* typ list -> typ -> int *)
     fun aux avoid T =
@@ -928,12 +938,12 @@
        | @{typ bool} => 2
        | @{typ unit} => 1
        | Type _ =>
-         (case datatype_constrs thy T of
+         (case datatype_constrs ext_ctxt T of
             [] => if is_integer_type T then 0 else raise SAME ()
           | constrs =>
             let
               val constr_cards =
-                datatype_constrs thy T
+                datatype_constrs ext_ctxt T
                 |> map (Integer.prod o map (aux (T :: avoid)) o binder_types
                         o snd)
             in
@@ -944,8 +954,9 @@
       handle SAME () => AList.lookup (op =) asgns T |> the_default default_card
   in Int.min (max, aux [] T) end
 
-(* theory -> typ -> bool *)
-fun is_finite_type thy = not_equal 0 o bounded_precise_card_of_type thy 1 2 []
+(* extended_context -> typ -> bool *)
+fun is_finite_type ext_ctxt =
+  not_equal 0 o bounded_precise_card_of_type ext_ctxt 1 2 []
 
 (* term -> bool *)
 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
@@ -1280,25 +1291,26 @@
     list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))
                              (index_seq 0 (length arg_Ts)) arg_Ts)
   end
-(* theory -> typ -> int * styp -> term -> term *)
-fun add_constr_case thy res_T (j, x) res_t =
+(* extended_context -> typ -> int * styp -> term -> term *)
+fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t =
   Const (@{const_name If}, [bool_T, res_T, res_T] ---> res_T)
-  $ discriminate_value thy x (Bound 0) $ constr_case_body thy (j, x) $ res_t
-(* theory -> typ -> typ -> term *)
-fun optimized_case_def thy dataT res_T =
+  $ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x)
+  $ res_t
+(* extended_context -> typ -> typ -> term *)
+fun optimized_case_def (ext_ctxt as {thy, ...}) dataT res_T =
   let
-    val xs = datatype_constrs thy dataT
+    val xs = datatype_constrs ext_ctxt dataT
     val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
     val (xs', x) = split_last xs
   in
     constr_case_body thy (1, x)
-    |> fold_rev (add_constr_case thy res_T) (length xs downto 2 ~~ xs')
+    |> fold_rev (add_constr_case ext_ctxt res_T) (length xs downto 2 ~~ xs')
     |> fold_rev (curry absdummy) (func_Ts @ [dataT])
   end
 
-(* theory -> string -> typ -> typ -> term -> term *)
-fun optimized_record_get thy s rec_T res_T t =
-  let val constr_x = the_single (datatype_constrs thy rec_T) in
+(* extended_context -> string -> typ -> typ -> term -> term *)
+fun optimized_record_get (ext_ctxt as {thy, ...}) s rec_T res_T t =
+  let val constr_x = the_single (datatype_constrs ext_ctxt rec_T) in
     case no_of_record_field thy s rec_T of
       ~1 => (case rec_T of
                Type (_, Ts as _ :: _) =>
@@ -1307,16 +1319,16 @@
                  val j = num_record_fields thy rec_T - 1
                in
                  select_nth_constr_arg thy constr_x t j res_T
-                 |> optimized_record_get thy s rec_T' res_T
+                 |> optimized_record_get ext_ctxt s rec_T' res_T
                end
              | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
                                 []))
     | j => select_nth_constr_arg thy constr_x t j res_T
   end
-(* theory -> string -> typ -> term -> term -> term *)
-fun optimized_record_update thy s rec_T fun_t rec_t =
+(* extended_context -> string -> typ -> term -> term -> term *)
+fun optimized_record_update (ext_ctxt as {thy, ...}) s rec_T fun_t rec_t =
   let
-    val constr_x as (_, constr_T) = the_single (datatype_constrs thy rec_T)
+    val constr_x as (_, constr_T) = the_single (datatype_constrs ext_ctxt rec_T)
     val Ts = binder_types constr_T
     val n = length Ts
     val special_j = no_of_record_field thy s rec_T
@@ -1327,7 +1339,7 @@
                         if j = special_j then
                           betapply (fun_t, t)
                         else if j = n - 1 andalso special_j = ~1 then
-                          optimized_record_update thy s
+                          optimized_record_update ext_ctxt s
                               (rec_T |> dest_Type |> snd |> List.last) fun_t t
                         else
                           t
@@ -1471,7 +1483,7 @@
           val (const, ts) =
             if is_built_in_const fast_descrs x then
               if s = @{const_name finite} then
-                if is_finite_type thy (domain_type T) then
+                if is_finite_type ext_ctxt (domain_type T) then
                   (Abs ("A", domain_type T, @{const True}), ts)
                 else case ts of
                   [Const (@{const_name UNIV}, _)] => (@{const False}, [])
@@ -1484,7 +1496,7 @@
                 val (dataT, res_T) = nth_range_type n T
                                      |> domain_type pairf range_type
               in
-                (optimized_case_def thy dataT res_T
+                (optimized_case_def ext_ctxt dataT res_T
                  |> do_term (depth + 1) Ts, ts)
               end
             | _ =>
@@ -1493,15 +1505,14 @@
               else if is_record_get thy x then
                 case length ts of
                   0 => (do_term depth Ts (eta_expand Ts t 1), [])
-                | _ => (optimized_record_get thy s (domain_type T)
+                | _ => (optimized_record_get ext_ctxt s (domain_type T)
                                              (range_type T) (hd ts), tl ts)
               else if is_record_update thy x then
                 case length ts of
-                  2 => (optimized_record_update thy (unsuffix Record.updateN s)
-                                                (nth_range_type 2 T)
-                                                (do_term depth Ts (hd ts))
-                                                (do_term depth Ts (nth ts 1)),
-                        [])
+                  2 => (optimized_record_update ext_ctxt
+                            (unsuffix Record.updateN s) (nth_range_type 2 T)
+                            (do_term depth Ts (hd ts))
+                            (do_term depth Ts (nth ts 1)), [])
                 | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
               else if is_rep_fun thy x then
                 let val x' = mate_of_rep_fun thy x in
@@ -1528,10 +1539,10 @@
         in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
   in do_term 0 [] end
 
-(* theory -> typ -> term list *)
-fun codatatype_bisim_axioms thy T =
+(* extended_context -> typ -> term list *)
+fun codatatype_bisim_axioms (ext_ctxt as {thy, ...}) T =
   let
-    val xs = datatype_constrs thy T
+    val xs = datatype_constrs ext_ctxt T
     val set_T = T --> bool_T
     val iter_T = @{typ bisim_iterator}
     val bisim_const = Const (@{const_name bisim}, [iter_T, T, T] ---> bool_T)
@@ -1554,14 +1565,14 @@
       let
         val arg_Ts = binder_types T
         val core_t =
-          discriminate_value thy x y_var ::
+          discriminate_value ext_ctxt x y_var ::
           map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
           |> foldr1 s_conj
       in List.foldr absdummy core_t arg_Ts end
   in
     [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
      $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
-        $ (betapplys (optimized_case_def thy T bool_T,
+        $ (betapplys (optimized_case_def ext_ctxt T bool_T,
                       map case_func xs @ [x_var]))),
      HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
      $ (Const (@{const_name insert}, [T, set_T] ---> set_T)
@@ -1621,11 +1632,11 @@
                         ScnpReconstruct.sizechange_tac]
 
 (* extended_context -> const_table -> styp -> bool *)
-fun is_is_well_founded_inductive_pred
+fun uncached_is_well_founded_inductive_pred
         ({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
          : extended_context) (x as (_, T)) =
   case def_props_for_const thy fast_descrs intro_table x of
-    [] => raise TERM ("Nitpick_HOL.is_is_well_founded_inductive_pred",
+    [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
                       [Const x])
   | intro_ts =>
     (case map (triple_for_intro_rule thy x) intro_ts
@@ -1677,7 +1688,7 @@
                 | NONE =>
                   let
                     val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
-                    val wf = is_is_well_founded_inductive_pred ext_ctxt x
+                    val wf = uncached_is_well_founded_inductive_pred ext_ctxt x
                   in
                     Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
                   end
@@ -1987,8 +1998,8 @@
                                                          seen, concl)
   end
 
-(* theory -> bool -> term -> term *)
-fun destroy_pulled_out_constrs thy axiom t =
+(* extended_context -> bool -> term -> term *)
+fun destroy_pulled_out_constrs (ext_ctxt as {thy, ...}) axiom t =
   let
     (* styp -> int *)
     val num_occs_of_var =
@@ -2022,7 +2033,7 @@
               andalso (not careful orelse not (is_Var t1)
                        orelse String.isPrefix val_var_prefix
                                               (fst (fst (dest_Var t1)))) then
-             discriminate_value thy x t1 ::
+             discriminate_value ext_ctxt x t1 ::
              map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
              |> foldr1 s_conj
              |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop
@@ -2711,7 +2722,7 @@
         | (Type (new_s, new_Ts as [new_T1, new_T2]),
            Type (old_s, old_Ts as [old_T1, old_T2])) =>
           if old_s mem [@{type_name fun_box}, @{type_name pair_box}, "*"] then
-            case constr_expand thy old_T t of
+            case constr_expand ext_ctxt old_T t of
               Const (@{const_name FunBox}, _) $ t1 =>
               if new_s = "fun" then
                 coerce_term Ts new_T (Type ("fun", old_Ts)) t1
@@ -3054,7 +3065,7 @@
         #> (if is_pure_typedef thy T then
               fold (add_def_axiom depth) (optimized_typedef_axioms thy z)
             else if max_bisim_depth >= 0 andalso is_codatatype thy T then
-              fold (add_def_axiom depth) (codatatype_bisim_axioms thy T)
+              fold (add_def_axiom depth) (codatatype_bisim_axioms ext_ctxt T)
             else
               I)
     (* int -> typ -> sort -> accumulator -> accumulator *)
@@ -3298,7 +3309,7 @@
       #> maybe_box ? box_fun_and_pair_in_term ext_ctxt def
       #> destroy_constrs ? (pull_out_universal_constrs thy def
                             #> pull_out_existential_constrs thy
-                            #> destroy_pulled_out_constrs thy def)
+                            #> destroy_pulled_out_constrs ext_ctxt def)
       #> curry_assms
       #> destroy_universal_equalities
       #> destroy_existential_equalities thy

--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Nov 05 17:00:28 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Nov 05 17:03:22 2009 +0100
@@ -530,7 +530,7 @@
                        evals, case_names, def_table, nondef_table, user_nondefs,
                        simp_table, psimp_table, intro_table, ground_thm_table,
                        ersatz_table, skolems, special_funs, unrolled_preds,
-                       wf_cache},
+                       wf_cache, constr_cache},
          card_assigns, bisim_depth, datatypes, ofs} : scope) formats all_frees
         free_names sel_names nonsel_names rel_table bounds =
   let
@@ -548,7 +548,7 @@
        intro_table = intro_table, ground_thm_table = ground_thm_table,
        ersatz_table = ersatz_table, skolems = skolems,
        special_funs = special_funs, unrolled_preds = unrolled_preds,
-       wf_cache = wf_cache}
+       wf_cache = wf_cache, constr_cache = constr_cache}
     val scope = {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
                  bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
     (* typ -> typ -> rep -> int list list -> term *)

--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Nov 05 17:00:28 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Nov 05 17:03:22 2009 +0100
@@ -215,7 +215,7 @@
           | NONE =>
             let
               val _ = Unsynchronized.change datatype_cache (cons (z, CRec z))
-              val xs = datatype_constrs thy T
+              val xs = datatype_constrs ext_ctxt T
               val (all_Cs, constr_Cs) =
                 fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) =>
                              let

--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Nov 05 17:00:28 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Nov 05 17:03:22 2009 +0100
@@ -45,7 +45,7 @@
   val all_scopes :
     extended_context -> int -> (typ option * int list) list
     -> (styp option * int list) list -> (styp option * int list) list
-    -> int list -> typ list -> typ list -> typ list -> scope list
+    -> int list -> typ list -> typ list -> typ list -> int * scope list
 end;
 
 structure Nitpick_Scope : NITPICK_SCOPE =
@@ -224,33 +224,31 @@
   SOME (Max constr, lookup_const_ints_assign thy maxes_asgns constr)
   handle TERM ("lookup_const_ints_assign", _) => NONE
 
-(* Proof.context -> (typ option * int list) list
+(* extended_context -> (typ option * int list) list
    -> (styp option * int list) list -> (styp option * int list) list -> int list
    -> typ -> block *)
-fun block_for_type ctxt cards_asgns maxes_asgns iters_asgns bisim_depths T =
-  let val thy = ProofContext.theory_of ctxt in
-    if T = @{typ bisim_iterator} then
-      [(Card T, map (fn k => Int.max (0, k) + 1) bisim_depths)]
-    else if is_fp_iterator_type T then
-      [(Card T, map (fn k => Int.max (0, k) + 1)
-                    (lookup_const_ints_assign thy iters_asgns
-                                              (const_for_iterator_type T)))]
-    else
-      (Card T, lookup_type_ints_assign thy cards_asgns T) ::
-      (case datatype_constrs thy T of
-         [_] => []
-       | constrs => map_filter (row_for_constr thy maxes_asgns) constrs)
-  end
+fun block_for_type (ext_ctxt as {thy, ...}) cards_asgns maxes_asgns iters_asgns
+                   bisim_depths T =
+  if T = @{typ bisim_iterator} then
+    [(Card T, map (fn k => Int.max (0, k) + 1) bisim_depths)]
+  else if is_fp_iterator_type T then
+    [(Card T, map (fn k => Int.max (0, k) + 1)
+                  (lookup_const_ints_assign thy iters_asgns
+                                            (const_for_iterator_type T)))]
+  else
+    (Card T, lookup_type_ints_assign thy cards_asgns T) ::
+    (case datatype_constrs ext_ctxt T of
+       [_] => []
+     | constrs => map_filter (row_for_constr thy maxes_asgns) constrs)
 
-(* Proof.context -> (typ option * int list) list
+(* extended_context -> (typ option * int list) list
    -> (styp option * int list) list -> (styp option * int list) list -> int list
    -> typ list -> typ list -> block list *)
-fun blocks_for_types ctxt cards_asgns maxes_asgns iters_asgns bisim_depths
+fun blocks_for_types ext_ctxt cards_asgns maxes_asgns iters_asgns bisim_depths
                      mono_Ts nonmono_Ts =
   let
-    val thy = ProofContext.theory_of ctxt
     (* typ -> block *)
-    val block_for = block_for_type ctxt cards_asgns maxes_asgns iters_asgns
+    val block_for = block_for_type ext_ctxt cards_asgns maxes_asgns iters_asgns
                                    bisim_depths
     val mono_block = maps block_for mono_Ts
     val nonmono_blocks = map block_for nonmono_Ts
@@ -291,15 +289,15 @@
 
 type scope_desc = (typ * int) list * (styp * int) list
 
-(* theory -> scope_desc -> typ * int -> bool *)
-fun is_surely_inconsistent_card_assign thy (card_asgns, max_asgns) (T, k) =
-  case datatype_constrs thy T of
+(* extended_context -> scope_desc -> typ * int -> bool *)
+fun is_surely_inconsistent_card_assign ext_ctxt (card_asgns, max_asgns) (T, k) =
+  case datatype_constrs ext_ctxt T of
     [] => false
   | xs =>
     let
       val precise_cards =
         map (Integer.prod
-             o map (bounded_precise_card_of_type thy k 0 card_asgns)
+             o map (bounded_precise_card_of_type ext_ctxt k 0 card_asgns)
              o binder_types o snd) xs
       val maxes = map (constr_max max_asgns) xs
       (* int -> int -> int *)
@@ -319,18 +317,19 @@
     end
     handle TYPE ("Nitpick_HOL.card_of_type", _, _) => false
 
-(* theory -> scope_desc -> bool *)
-fun is_surely_inconsistent_scope_description thy (desc as (card_asgns, _)) =
-  exists (is_surely_inconsistent_card_assign thy desc) card_asgns
+(* extended_context -> scope_desc -> bool *)
+fun is_surely_inconsistent_scope_description ext_ctxt
+                                             (desc as (card_asgns, _)) =
+  exists (is_surely_inconsistent_card_assign ext_ctxt desc) card_asgns
 
-(* theory -> scope_desc -> (typ * int) list option *)
-fun repair_card_assigns thy (card_asgns, max_asgns) =
+(* extended_context -> scope_desc -> (typ * int) list option *)
+fun repair_card_assigns ext_ctxt (card_asgns, max_asgns) =
   let
     (* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
     fun aux seen [] = SOME seen
       | aux seen ((T, 0) :: _) = NONE
       | aux seen ((T, k) :: asgns) =
-        (if is_surely_inconsistent_scope_description thy
+        (if is_surely_inconsistent_scope_description ext_ctxt
                 ((T, k) :: seen, max_asgns) then
            raise SAME ()
          else
@@ -362,12 +361,12 @@
 (* block -> scope_desc *)
 fun scope_descriptor_from_block block =
   fold_rev add_row_to_scope_descriptor block ([], [])
-(* theory -> block list -> int list -> scope_desc option *)
-fun scope_descriptor_from_combination thy blocks columns =
+(* extended_context -> block list -> int list -> scope_desc option *)
+fun scope_descriptor_from_combination (ext_ctxt as {thy, ...}) blocks columns =
   let
     val (card_asgns, max_asgns) =
       maps project_block (columns ~~ blocks) |> scope_descriptor_from_block
-    val card_asgns = repair_card_assigns thy (card_asgns, max_asgns) |> the
+    val card_asgns = repair_card_assigns ext_ctxt (card_asgns, max_asgns) |> the
   in
     SOME (map (repair_iterator_assign thy card_asgns) card_asgns, max_asgns)
   end
@@ -443,7 +442,7 @@
     val self_recs = map (is_self_recursive_constr_type o snd) xs
     val (num_self_recs, num_non_self_recs) =
       List.partition (equal true) self_recs |> pairself length
-    val precise = (card = bounded_precise_card_of_type thy (card + 1) 0
+    val precise = (card = bounded_precise_card_of_type ext_ctxt (card + 1) 0
                                                        card_asgns T)
     (* int -> int *)
     fun sum_dom_cards max =
@@ -483,23 +482,27 @@
   | fix_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_asgns) =
     (NONE, ks) :: fix_cards_assigns_wrt_boxing thy Ts cards_asgns
 
+val max_scopes = 4096
 val distinct_threshold = 512
 
 (* extended_context -> int -> (typ option * int list) list
    -> (styp option * int list) list -> (styp option * int list) list -> int list
-   -> typ list -> typ list -> typ list -> scope list *)
-fun all_scopes (ext_ctxt as {thy, ctxt, ...}) sym_break cards_asgns maxes_asgns
+   -> typ list -> typ list -> typ list -> int * scope list *)
+fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_asgns maxes_asgns
                iters_asgns bisim_depths mono_Ts nonmono_Ts shallow_dataTs =
   let
     val cards_asgns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_asgns
-    val blocks = blocks_for_types ctxt cards_asgns maxes_asgns iters_asgns
+    val blocks = blocks_for_types ext_ctxt cards_asgns maxes_asgns iters_asgns
                                   bisim_depths mono_Ts nonmono_Ts
     val ranks = map rank_of_block blocks
-    val descs = all_combinations_ordered_smartly (map (rpair 0) ranks)
-                |> map_filter (scope_descriptor_from_combination thy blocks)
+    val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
+    val head = Library.take (max_scopes, all)
+    val descs = map_filter (scope_descriptor_from_combination ext_ctxt blocks)
+                           head
   in
-    descs |> length descs <= distinct_threshold ? distinct (op =)
-          |> map (scope_from_descriptor ext_ctxt sym_break shallow_dataTs)
+    (length all - length head,
+     descs |> length descs <= distinct_threshold ? distinct (op =)
+           |> map (scope_from_descriptor ext_ctxt sym_break shallow_dataTs))
   end
 
 end;