diff -r 6f9f80afaf4f -r 747f8077b09a src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Aug 03 14:54:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Aug 03 15:15:17 2010 +0200
@@ -17,7 +17,7 @@
   val univ_card :
     int -> int -> int -> Kodkod.bound list -> Kodkod.formula -> int
   val check_bits : int -> Kodkod.formula -> unit
-  val check_arity : int -> int -> unit
+  val check_arity : string -> int -> int -> unit
   val kk_tuple : bool -> int -> int list -> Kodkod.tuple
   val tuple_set_from_atom_schema : (int * int) list -> Kodkod.tuple_set
   val sequential_int_bounds : int -> Kodkod.int_bound list
@@ -93,11 +93,17 @@
                   int_expr_func = int_expr_func}
   in KK.fold_formula expr_F formula () end
 
-fun check_arity univ_card n =
+fun check_arity guilty_party univ_card n =
   if n > KK.max_arity univ_card then
     raise TOO_LARGE ("Nitpick_Kodkod.check_arity",
-                     "arity " ^ string_of_int n ^ " too large for universe of \
-                     \cardinality " ^ string_of_int univ_card)
+                     "arity " ^ string_of_int n ^
+                     (if guilty_party = "" then
+                        ""
+                      else
+                        " of Kodkod relation associated with " ^
+                        quote guilty_party) ^
+                     " too large for universe of cardinality " ^
+                     string_of_int univ_card)
   else
     ()
 
@@ -200,7 +206,7 @@
 
 fun tabulate_built_in_rel debug ofs univ_card nat_card int_card j0
                           (x as (n, _)) =
-  (check_arity univ_card n;
+  (check_arity "" univ_card n;
    if x = not3_rel then
      ("not3", tabulate_func1 debug univ_card (2, j0) (curry (op -) 1))
    else if x = suc_rel then