1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 02 18:52:51 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 02 19:15:15 2010 +0200
     1.3 @@ -2088,6 +2088,10 @@
     1.4      |> unfold_defs_in_term hol_ctxt
     1.5    end
     1.6  
     1.7 +fun is_good_starred_linear_pred_type (Type (@{type_name fun}, Ts)) =
     1.8 +    forall (not o (is_fun_type orf is_pair_type)) Ts
     1.9 +  | is_good_starred_linear_pred_type _ = false
    1.10 +
    1.11  fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
    1.12                                                  def_table, simp_table, ...})
    1.13                                    gfp (x as (s, T)) =
    1.14 @@ -2099,8 +2103,9 @@
    1.15    in
    1.16      if is_equational_fun hol_ctxt x' then
    1.17        unrolled_const (* already done *)
    1.18 -    else if not gfp andalso is_linear_inductive_pred_def def andalso
    1.19 -         star_linear_preds then
    1.20 +    else if not gfp andalso star_linear_preds andalso
    1.21 +         is_linear_inductive_pred_def def andalso
    1.22 +         is_good_starred_linear_pred_type T then
    1.23        starred_linear_pred_const hol_ctxt x def
    1.24      else
    1.25        let