src/HOL/Tools/Nitpick/nitpick_hol.ML

                  @{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse
   let
     val thy = ProofContext.theory_of ctxt
     val (x as (_, T)) = (s, unarize_unbox_etc_type T)
   in
-    Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
+    is_real_constr thy x orelse is_record_constr x orelse
     (is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse
     is_coconstr thy x
   end
 fun is_stale_constr ctxt (x as (_, T)) =
   let val thy = ProofContext.theory_of ctxt in

          case Datatype.get_info thy s of
            SOME {index, descr, ...} =>
            let
              val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
            in
-             map (fn (s', Us) =>
-                     (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
-                          ---> T)) constrs
+             map (apsnd (fn Us =>
+                            map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
+                 constrs
            end
          | NONE =>
            if is_record_type T then
              let
                val s' = unsuffix Record.ext_typeN s ^ Record.extN