src/HOL/Tools/Nitpick/nitpick.ML

     val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy 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
+    val user_nondefs =
+      user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
     val intro_table = inductive_intro_table ctxt subst def_table
     val ground_thm_table = ground_theorem_table thy
     val ersatz_table = ersatz_table thy
     val (hol_ctxt as {wf_cache, ...}) =
       {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,

        star_linear_preds = star_linear_preds, uncurry = uncurry,
        fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
        case_names = case_names, def_table = def_table,
        nondef_table = nondef_table, user_nondefs = user_nondefs,
        simp_table = simp_table, psimp_table = psimp_table,
-       intro_table = intro_table, ground_thm_table = ground_thm_table,
-       ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
-       special_funs = Unsynchronized.ref [],
+       choice_spec_table = choice_spec_table, 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 [],
        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"