diff -r 384d6d48a7d3 -r 2746dfc9ceae src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 06 09:43:25 2024 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Feb 27 13:46:42 2024 +0100
@@ -202,7 +202,6 @@
     val time_start = Time.now ()
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
-    val keywords = Thy_Header.get_keywords thy
     val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
          boxes, finitizes, monos, wfs, sat_solver, falsify, debug, verbose,
          overlord, spy, user_axioms, assms, whacks, merge_type_vars,
@@ -342,7 +341,7 @@
 
     val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
     fun monotonicity_message Ts extra =
-      let val pretties = map (pretty_maybe_quote keywords o pretty_for_type ctxt) Ts in
+      let val pretties = map (pretty_maybe_quote ctxt o pretty_for_type ctxt) Ts in
         Pretty.blk (0,
           Pretty.text ("The type" ^ plural_s_for_list pretties) @ [Pretty.brk 1] @
           pretty_serial_commas "and" pretties @ [Pretty.brk 1] @