src/HOL/Tools/Nitpick/nitpick_hol.ML

   val const_match : theory -> styp * styp -> bool
   val term_match : theory -> term * term -> bool
   val frac_from_term_pair : typ -> term -> term -> term
   val is_TFree : typ -> bool
   val is_fun_type : typ -> bool
+  val is_set_type : typ -> bool
+  val is_fun_or_set_type : typ -> bool
   val is_set_like_type : typ -> bool
   val is_pair_type : typ -> bool
   val is_lfp_iterator_type : typ -> bool
   val is_gfp_iterator_type : typ -> bool
   val is_fp_iterator_type : typ -> bool

 
 fun is_TFree (TFree _) = true
   | is_TFree _ = false
 fun is_fun_type (Type (@{type_name fun}, _)) = true
   | is_fun_type _ = false
-fun is_set_like_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
+fun is_set_type (Type (@{type_name set}, _)) = true
+  | is_set_type _ = false
+val is_fun_or_set_type = is_fun_type orf is_set_type
+fun is_set_like_type (Type (@{type_name fun}, [_, T'])) =
+    (body_type T' = bool_T)
   | is_set_like_type (Type (@{type_name set}, _)) = true
   | is_set_like_type _ = false
 fun is_pair_type (Type (@{type_name prod}, _)) = true
   | is_pair_type _ = false
 fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s

 fun is_frac_type ctxt (Type (s, [])) =
     s |> AList.defined (op =) (#frac_types (Data.get (Context.Proof ctxt)))
   | is_frac_type _ _ = false
 fun is_number_type ctxt = is_integer_like_type orf is_frac_type ctxt
 fun is_higher_order_type (Type (@{type_name fun}, _)) = true
+  | is_higher_order_type (Type (@{type_name set}, _)) = true
   | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
   | is_higher_order_type _ = false
 
 fun elem_type (Type (@{type_name set}, [T'])) = T'
   | elem_type T = raise TYPE ("Nitpick_HOL.elem_type", [T], [])

   in do_term 0 [] end
 
 (** Axiom extraction/generation **)
 
 fun extensional_equal j T t1 t2 =
-  if is_fun_type T orelse is_set_like_type T then
+  if is_fun_or_set_type T then
     let
       val dom_T = pseudo_domain_type T
       val ran_T = pseudo_range_type T
       val var_t = Var (("x", j), dom_T)
       fun apply fun_t arg_t =

     list_abs (outer, image_set |> ap_curry tuple_arg_Ts tuple_T)
     |> unfold_defs_in_term hol_ctxt
   end
 
 fun is_good_starred_linear_pred_type (Type (@{type_name fun}, Ts)) =
-    forall (not o (is_fun_type orf is_pair_type)) Ts
+    forall (not o (is_fun_or_set_type orf is_pair_type)) Ts
   | is_good_starred_linear_pred_type _ = false
 
 fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
                                                 def_tables, simp_table, ...})
                                   gfp (x as (s, T)) =