# HG changeset patch
# User blanchet
# Date 1325611998 -3600
# Node ID 30711d9b686ea5f1e0d87308f34cede5a6ba7446
# Parent  40ac5ae6d16f5b4bd3e7bf90aa41bc3025d85608
handle "Id" gracefully w.r.t. "set"

diff -r 40ac5ae6d16f -r 30711d9b686e src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Jan 03 18:33:18 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Jan 03 18:33:18 2012 +0100
@@ -940,7 +940,7 @@
                            (rel_expr_from_rel_expr kk min_R R2 r2))
           end
       | Cst (Iden, _, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0
-      | Cst (Iden, T as Type (@{type_name fun}, [T1, _]), R as Func (R1, _)) =>
+      | Cst (Iden, T as Type (@{type_name set}, [T1]), R as Func (R1, _)) =>
         to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut)))
       | Cst (Num j, T, R) =>
         if is_word_type T then