improved precision of "set" based on an example from Lukas
authorblanchet
Tue, 01 Jun 2010 15:53:15 +0200
changeset 37266 773dc74118f6
parent 37265 9f2c3d3c8f0f
child 37267 5c47d633c84d
improved precision of "set" based on an example from Lukas
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