src/HOL/Nitpick_Examples/Mono_Nits.thy

    psimp_table = Symtab.empty, intro_table = Symtab.empty,
    ground_thm_table = Inttab.empty, ersatz_table = [],
    skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
    unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref []}
 (* term -> bool *)
-val is_mono = NitpickMono.formulas_monotonic ext_ctxt @{typ 'a} [] []
+val is_mono = Nitpick_Mono.formulas_monotonic ext_ctxt @{typ 'a} [] []
 fun is_const t =
   let val T = fastype_of t in
     is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
                                @{const False}))
   end