--- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Aug 06 11:05:57 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Aug 06 11:33:58 2010 +0200
@@ -365,14 +365,25 @@
exists (curry (op =) T o domain_type o type_of) sel_names
val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
|> sort Term_Ord.typ_ord
- val _ = if verbose andalso binary_ints = SOME true andalso
- exists (member (op =) [nat_T, int_T]) all_Ts then
- print_v (K "The option \"binary_ints\" will be ignored because \
- \of the presence of rationals, reals, \"Suc\", \
- \\"gcd\", or \"lcm\" in the problem or because of the \
- \\"non_std\" option.")
- else
- ()
+ val _ =
+ if verbose andalso binary_ints = SOME true andalso
+ exists (member (op =) [nat_T, int_T]) all_Ts then
+ print_v (K "The option \"binary_ints\" will be ignored because of the \
+ \presence of rationals, reals, \"Suc\", \"gcd\", or \"lcm\" \
+ \in the problem or because of the \"non_std\" option.")
+ else
+ ()
+ val _ =
+ if not auto andalso
+ exists (fn Type (@{type_name Datatype.node}, _) => true | _ => false)
+ all_Ts then
+ print_m (K ("Warning: The problem involves directly or indirectly the \
+ \internal type " ^ quote @{type_name Datatype.node} ^
+ ". This type is very Nitpick-unfriendly, and its presence \
+ \usually indicates either a failure in abstraction or a \
+ \bug in Nitpick."))
+ else
+ ()
val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
val _ =
if verbose andalso not unique_scope then