src/HOL/Tools/Nitpick/nitpick.ML

      max_threads: int,
      show_datatypes: bool,
      show_consts: bool,
      evals: term list,
      formats: (term option * int list) list,
+     atomss: (typ option * string list) list,
      max_potential: int,
      max_genuine: int,
      check_potential: bool,
      check_genuine: bool,
      batch_size: int,

    max_threads: int,
    show_datatypes: bool,
    show_consts: bool,
    evals: term list,
    formats: (term option * int list) list,
+   atomss: (typ option * string list) list,
    max_potential: int,
    max_genuine: int,
    check_potential: bool,
    check_genuine: bool,
    batch_size: int,

     val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
          boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
          verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
          destroy_constrs, specialize, star_linear_preds, fast_descrs,
          peephole_optim, tac_timeout, max_threads, show_datatypes, show_consts,
-         evals, formats, max_potential, max_genuine, check_potential,
+         evals, formats, atomss, max_potential, max_genuine, check_potential,
          check_genuine, batch_size, ...} = params
     val state_ref = Unsynchronized.ref state
     val pprint =
       if auto then
         Unsynchronized.change state_ref o Proof.goal_message o K

     val (assms_t, evals) =
       assms_t :: evals |> merge_type_vars ? merge_type_vars_in_terms
                        |> pairf hd tl
     val original_max_potential = max_potential
     val original_max_genuine = max_genuine
-(*
-    val _ = print_g ("*** " ^ Syntax.string_of_term ctxt orig_t)
-    val _ = List.app (fn t => print_g ("*** " ^ Syntax.string_of_term ctxt t))
-                     orig_assm_ts
-*)
     val max_bisim_depth = fold Integer.max bisim_depths ~1
     val case_names = case_const_names thy stds
-    val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy subst
+    val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst
     val def_table = const_def_table ctxt subst defs
     val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
     val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
     val psimp_table = const_psimp_table ctxt subst
     val choice_spec_table = const_choice_spec_table ctxt subst

          else
            (if length ss = 1 then "is" else "are") ^ " considered monotonic") ^
         ". " ^ extra
       end
     fun is_type_fundamentally_monotonic T =
-      (is_datatype thy stds T andalso not (is_quot_type thy T) andalso
-       (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
+      (is_datatype ctxt stds T andalso not (is_quot_type thy T) andalso
+       (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
       is_number_type thy T orelse is_bit_type T
     fun is_type_actually_monotonic T =
       formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
     fun is_type_kind_of_monotonic T =
       case triple_lookup (type_match thy) monos T of

           print_v (K (monotonicity_message interesting_mono_Ts
                          "Nitpick might be able to skip some scopes."))
       else
         ()
     val (deep_dataTs, shallow_dataTs) =
-      all_Ts |> filter (is_datatype thy stds) |> List.partition is_datatype_deep
+      all_Ts |> filter (is_datatype ctxt stds)
+             |> List.partition is_datatype_deep
     val finitizable_dataTs =
       shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
                      |> filter is_shallow_datatype_finitizable
     val _ =
       if verbose andalso not (null finitizable_dataTs) then

              : problem_extension) =
       let
         val (reconstructed_model, codatatypes_ok) =
           reconstruct_hol_model {show_datatypes = show_datatypes,
                                  show_consts = show_consts}
-              scope formats frees free_names sel_names nonsel_names rel_table
-              bounds
+              scope formats atomss frees free_names sel_names nonsel_names
+              rel_table bounds
         val genuine_means_genuine =
           got_all_user_axioms andalso none_true wfs andalso
           sound_finitizes andalso codatatypes_ok
       in
         (pprint (Pretty.chunks