diff -r 4c39632b811f -r 8580ba651489 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Feb 17 10:28:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Feb 17 11:19:48 2010 +0100
@@ -382,29 +382,22 @@
       else
         ()
     val deep_dataTs = filter is_deep_datatype all_Ts
-    (* FIXME: Implement proper detection of induction datatypes. *)
+    (* This detection code is an ugly hack. Fortunately, it is used only to
+       provide a hint to the user. *)
     (* string * (Rule_Cases.T * bool) -> bool *)
-    fun is_inductive_case (_, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
-      false
-(*
-      not (null fixes) andalso exists (String.isSuffix ".hyps" o fst) assumes
-*)
-    (* unit -> typ list *)
-    val induct_dataTs =
-      if exists is_inductive_case (ProofContext.cases_of ctxt) then
-        filter (is_datatype thy) all_Ts
-      else
-        []
-    val _ = if standard andalso not (null induct_dataTs) then
+    fun is_struct_induct_step (name, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
+      not (null fixes) andalso
+      exists (String.isSuffix ".hyps" o fst) assumes andalso
+      exists (exists (curry (op =) name o shortest_name o fst)
+              o datatype_constrs hol_ctxt) deep_dataTs
+    val likely_in_struct_induct_step =
+      exists is_struct_induct_step (ProofContext.cases_of ctxt)
+    val _ = if standard andalso likely_in_struct_induct_step then
               pprint_m (fn () => Pretty.blk (0,
                   pstrs "Hint: To check that the induction hypothesis is \
                         \general enough, try this command: " @
                   [Pretty.mark Markup.sendback (Pretty.blk (0,
-                       pstrs ("nitpick [" ^
-                              commas (map (prefix "non_std " o maybe_quote
-                                           o unyxml o string_for_type ctxt)
-                                          induct_dataTs) ^
-                              ", show_consts]")))] @ pstrs "."))
+                       pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
             else
               ()
 (*
@@ -635,7 +628,7 @@
               | NONE => print "No confirmation by \"auto\".")
            else
              ();
-           if not standard andalso not (null induct_dataTs) then
+           if not standard andalso likely_in_struct_induct_step then
              print "The existence of a nonstandard model suggests that the \
                    \induction hypothesis is not general enough or perhaps even \
                    \wrong. See the \"Inductive Properties\" section of the \
@@ -874,7 +867,7 @@
           if max_potential = original_max_potential then
             (print_m (fn () =>
                  "Nitpick found no " ^ das_wort_model ^ "." ^
-                 (if not standard andalso not (null induct_dataTs) then
+                 (if not standard andalso likely_in_struct_induct_step then
                     " This suggests that the induction hypothesis might be \
                     \general enough to prove this subgoal."
                   else