# HG changeset patch
# User blanchet
# Date 1325675393 -3600
# Node ID e6d33b200f42055add4c330695de402c489a0434
# Parent  dd112cd72c489159c9e3433b3ee1b45fa108c9a6
remove subtlety whose justification got lost in time -- the new code is possibly less precise but sounder

diff -r dd112cd72c48 -r e6d33b200f42 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Jan 04 12:09:53 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Jan 04 12:09:53 2012 +0100
@@ -350,9 +350,7 @@
       fold add_free_and_const_names (nondef_us @ def_us @ need_us) ([], [])
     val (sel_names, nonsel_names) =
       List.partition (is_sel o nickname_of) const_names
-    val sound_finitizes =
-      none_true (filter_out (fn (SOME (Type (@{type_name fun}, _)), _) => true
-                          | _ => false) finitizes)
+    val sound_finitizes = none_true finitizes
     val standard = forall snd stds
 (*
     val _ =