Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 39360 cdf2c3341422
parent 39359 6f49c7fbb1b1
child 40058 b4f62d0660e0 
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Sep 14 13:24:18 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Sep 14 13:44:43 2010 +0200
@@ -711,8 +711,7 @@
                          MFun (a_to_b_set_M, S Minus, ab_set_M)), accum)
                 end
               | _ =>
-                if s = @{const_name safe_The} orelse
-                   s = @{const_name safe_Eps} then
+                if s = @{const_name safe_The} then
                   let
                     val a_set_M = mtype_for (domain_type T)
                     val a_M = dest_MFun a_set_M |> #1
isabelle