src/HOL/Tools/Nitpick/nitpick_scope.ML

 fun spec_of_type ({card_assigns, ofs, ...} : scope) T =
   (card_of_type card_assigns T
    handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
 
 fun quintuple_for_scope code_type code_term code_string
-        ({hol_ctxt = {ctxt, stds, ...}, card_assigns, bits, bisim_depth,
+        ({hol_ctxt = {ctxt = ctxt0, stds, ...}, card_assigns, bits, bisim_depth,
          datatypes, ...} : scope) =
   let
+    val ctxt = set_show_all_types ctxt0
     val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
                      @{typ bisim_iterator}]
     val (iter_assigns, card_assigns) =
       card_assigns |> filter_out (member (op =) boring_Ts o fst)
                    |> List.partition (is_fp_iterator_type o fst)

       (if bits = 0 then []
        else [code_string ("bits = " ^ string_of_int bits)]) @
       (if bisim_depth < 0 andalso forall (not o #co) datatypes then []
        else [code_string ("bisim_depth = " ^ signed_string_of_int bisim_depth)])
   in
-    setmp_show_all_types
-        (fn () => (cards primary_card_assigns, cards secondary_card_assigns,
-                   maxes (), iters (), miscs ())) ()
+    (cards primary_card_assigns, cards secondary_card_assigns,
+     maxes (), iters (), miscs ())
   end
 
 fun pretties_for_scope scope verbose =
   let
     fun standard_blocks s = map (Pretty.block o cons (Pretty.str (s ^ " ")))