--- 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