src/HOL/Tools/Nitpick/nitpick.ML

                            subst def_assm_ts nondef_assm_ts orig_t =
   let
     val timer = Timer.startRealTimer ()
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
+    val keywords = Thy_Header.get_keywords thy
 (* FIXME: reintroduce code before new release:
 
     val nitpick_thy = Thy_Info.get_theory "Nitpick"
     val _ = Theory.subthy (nitpick_thy, thy) orelse
             error "You must import the theory \"Nitpick\" to use Nitpick"

       List.app (print_g o string_for_nut ctxt) (nondef_us @ def_us @ need_us)
 *)
 
     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 o pretty_for_type ctxt) Ts in
+      let val pretties = map (pretty_maybe_quote keywords o pretty_for_type ctxt) Ts in
         Pretty.blk (0,
           pstrs ("The type" ^ plural_s_for_list pretties ^ " ") @
           pretty_serial_commas "and" pretties @
           pstrs (" " ^
                  (if none_true monos then