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