src/HOL/Tools/Nitpick/nitpick_scope.ML
changeset 35178 29a0e3be0be1
parent 35072 888802be2019
child 35179 4b198af5beb5
equal deleted inserted replaced
35177:168041f24f80 35178:29a0e3be0be1
   160                          (Const (const_for_iterator_type T))) ^ " = " ^
   160                          (Const (const_for_iterator_type T))) ^ " = " ^
   161               string_of_int (k - 1)) iter_assigns
   161               string_of_int (k - 1)) iter_assigns
   162     fun miscs () =
   162     fun miscs () =
   163       (if bits = 0 then [] else ["bits = " ^ string_of_int bits]) @
   163       (if bits = 0 then [] else ["bits = " ^ string_of_int bits]) @
   164       (if bisim_depth < 0 andalso forall (not o #co) datatypes then []
   164       (if bisim_depth < 0 andalso forall (not o #co) datatypes then []
   165        else ["bisim_depth = " ^ string_of_int bisim_depth])
   165        else ["bisim_depth = " ^ signed_string_of_int bisim_depth])
   166   in
   166   in
   167     setmp_show_all_types
   167     setmp_show_all_types
   168         (fn () => (cards primary_card_assigns, cards secondary_card_assigns,
   168         (fn () => (cards primary_card_assigns, cards secondary_card_assigns,
   169                    maxes (), iters (), miscs ())) ()
   169                    maxes (), iters (), miscs ())) ()
   170   end
   170   end