1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Aug 06 11:05:57 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Aug 06 11:33:58 2010 +0200
     1.3 @@ -365,14 +365,25 @@
     1.4        exists (curry (op =) T o domain_type o type_of) sel_names
     1.5      val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
     1.6                   |> sort Term_Ord.typ_ord
     1.7 -    val _ = if verbose andalso binary_ints = SOME true andalso
     1.8 -               exists (member (op =) [nat_T, int_T]) all_Ts then
     1.9 -              print_v (K "The option \"binary_ints\" will be ignored because \
    1.10 -                         \of the presence of rationals, reals, \"Suc\", \
    1.11 -                         \\"gcd\", or \"lcm\" in the problem or because of the \
    1.12 -                         \\"non_std\" option.")
    1.13 -            else
    1.14 -              ()
    1.15 +    val _ =
    1.16 +      if verbose andalso binary_ints = SOME true andalso
    1.17 +         exists (member (op =) [nat_T, int_T]) all_Ts then
    1.18 +        print_v (K "The option \"binary_ints\" will be ignored because of the \
    1.19 +                   \presence of rationals, reals, \"Suc\", \"gcd\", or \"lcm\" \
    1.20 +                   \in the problem or because of the \"non_std\" option.")
    1.21 +      else
    1.22 +        ()
    1.23 +    val _ =
    1.24 +      if not auto andalso
    1.25 +         exists (fn Type (@{type_name Datatype.node}, _) => true | _ => false)
    1.26 +                all_Ts then
    1.27 +        print_m (K ("Warning: The problem involves directly or indirectly the \
    1.28 +                    \internal type " ^ quote @{type_name Datatype.node} ^
    1.29 +                    ". This type is very Nitpick-unfriendly, and its presence \
    1.30 +                    \usually indicates either a failure in abstraction or a \
    1.31 +                    \bug in Nitpick."))
    1.32 +      else
    1.33 +        ()
    1.34      val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
    1.35      val _ =
    1.36        if verbose andalso not unique_scope then