diff -r a00685a18e55 -r 0ed9365fa9d2 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jan 03 18:33:18 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jan 03 18:33:18 2012 +0100
@@ -389,9 +389,9 @@
       | postprocess_subterms Ts t = postprocess_term (fastype_of1 (Ts, t)) t
     fun make_set maybe_opt T tps =
       let
-        val empty_const = Const (@{const_abbrev Set.empty}, T --> bool_T)
-        val insert_const =
-          Const (@{const_name insert}, T --> (T --> bool_T) --> T --> bool_T)
+        val set_T = HOLogic.mk_setT T
+        val empty_const = Const (@{const_abbrev Set.empty}, set_T)
+        val insert_const = Const (@{const_name insert}, T --> set_T --> set_T)
         fun aux [] =
             if maybe_opt andalso not (is_complete_type datatypes false T) then
               insert_const $ Const (unrep (), T) $ empty_const
@@ -408,7 +408,7 @@
       in
         if forall (fn (_, t) => t <> @{const True} andalso t <> @{const False})
                   tps then
-          Const (unknown, T --> bool_T)
+          Const (unknown, set_T)
         else
           aux tps
       end