# HG changeset patch
# User haftmann
# Date 1488105513 -3600
# Node ID 928156a95e1a0d1e71a73acc9e93fe0002e87415
# Parent  805d0a9a4e3769f5a34750386bc34d65e72e8b6a
clarified comment

diff -r 805d0a9a4e37 -r 928156a95e1a src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Feb 24 13:59:50 2017 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Feb 26 11:38:33 2017 +0100
@@ -714,10 +714,10 @@
        in
          case t_opt of
            SOME (Const (@{const_name top}, _)) => true
-           (* "Multiset.multiset" *)
+           (* "Multiset.multiset" FIXME unchecked *)
          | SOME (Const (@{const_name Collect}, _)
                  $ Abs (_, _, Const (@{const_name finite}, _) $ _)) => true
-           (* "FinFun.finfun" *)
+           (* "FinFun.finfun" FIXME unchecked *)
          | SOME (Const (@{const_name Collect}, _) $ Abs (_, _,
                      Const (@{const_name Ex}, _) $ Abs (_, _,
                          Const (@{const_name finite}, _) $ _))) => true