handle "Id" gracefully w.r.t. "set"
authorblanchet
Tue, 03 Jan 2012 18:33:18 +0100
changeset 46100 30711d9b686e
parent 46099 40ac5ae6d16f
child 46101 da17bfdadef6
handle "Id" gracefully w.r.t. "set"
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