# HG changeset patch
# User blanchet
# Date 1275400395 -7200
# Node ID 773dc74118f60ed925207784c907c1ab0a3ac97d
# Parent  9f2c3d3c8f0fca93d2f09b947182f7e03a1b46e5
improved precision of "set" based on an example from Lukas

diff -r 9f2c3d3c8f0f -r 773dc74118f6 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Jun 01 15:43:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Jun 01 15:53:15 2010 +0200
@@ -689,7 +689,8 @@
       forall is_fully_representable_set [u1, u2]
     else if oper = Apply then
       case u1 of
-        ConstName (s, _, _) => is_sel_like_and_no_discr s
+        ConstName (s, _, _) =>
+        is_sel_like_and_no_discr s orelse s = @{const_name set}
       | _ => false
     else
       false