# HG changeset patch
# User blanchet
# Date 1281087238 -7200
# Node ID 8164c91039eafa990d2e695fbc90a1155a1e0fd0
# Parent  d4cbc80e72713664882c38116b294a7f4919aa89
added a friendly warning

diff -r d4cbc80e7271 -r 8164c91039ea src/HOL/Tools/Nitpick/nitpick.ML
--- 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