careful about which linear inductive predicates should be starred

--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 02 18:52:51 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 02 19:15:15 2010 +0200
@@ -2088,6 +2088,10 @@
     |> unfold_defs_in_term hol_ctxt
   end
 
+fun is_good_starred_linear_pred_type (Type (@{type_name fun}, Ts)) =
+    forall (not o (is_fun_type orf is_pair_type)) Ts
+  | is_good_starred_linear_pred_type _ = false
+
 fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
                                                 def_table, simp_table, ...})
                                   gfp (x as (s, T)) =
@@ -2099,8 +2103,9 @@
   in
     if is_equational_fun hol_ctxt x' then
       unrolled_const (* already done *)
-    else if not gfp andalso is_linear_inductive_pred_def def andalso
-         star_linear_preds then
+    else if not gfp andalso star_linear_preds andalso
+         is_linear_inductive_pred_def def andalso
+         is_good_starred_linear_pred_type T then
       starred_linear_pred_const hol_ctxt x def
     else
       let