src/HOL/Tools/Nitpick/nitpick.ML
changeset 57996 ca917ea6969c
parent 56245 84fc7dfa3cd4
child 58843 521cea5fa777
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Aug 19 09:36:57 2014 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Aug 19 09:39:11 2014 +0200
     1.3 @@ -416,17 +416,6 @@
     1.4                     \in the problem.")
     1.5        else
     1.6          ()
     1.7 -    val _ =
     1.8 -      if mode = Normal andalso
     1.9 -         exists (fn Type (@{type_name Datatype.node}, _) => true | _ => false)
    1.10 -                all_Ts then
    1.11 -        print_nt (K ("Warning: The problem involves directly or indirectly the \
    1.12 -                     \internal type " ^ quote @{type_name Datatype.node} ^
    1.13 -                     ". This type is very Nitpick-unfriendly, and its presence \
    1.14 -                     \usually indicates either a failure of abstraction or a \
    1.15 -                     \quirk in Nitpick."))
    1.16 -      else
    1.17 -        ()
    1.18      val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
    1.19      val _ =
    1.20        if verbose andalso not unique_scope then