remove subtlety whose justification got lost in time -- the new code is possibly less precise but sounder
authorblanchet
Wed Jan 04 12:09:53 2012 +0100 (2012-01-04 ago)
changeset 46114e6d33b200f42
parent 46113 dd112cd72c48
child 46115 ecab67f5a5c2
remove subtlety whose justification got lost in time -- the new code is possibly less precise but sounder
src/HOL/Tools/Nitpick/nitpick.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Jan 04 12:09:53 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Jan 04 12:09:53 2012 +0100
     1.3 @@ -350,9 +350,7 @@
     1.4        fold add_free_and_const_names (nondef_us @ def_us @ need_us) ([], [])
     1.5      val (sel_names, nonsel_names) =
     1.6        List.partition (is_sel o nickname_of) const_names
     1.7 -    val sound_finitizes =
     1.8 -      none_true (filter_out (fn (SOME (Type (@{type_name fun}, _)), _) => true
     1.9 -                          | _ => false) finitizes)
    1.10 +    val sound_finitizes = none_true finitizes
    1.11      val standard = forall snd stds
    1.12  (*
    1.13      val _ =