# HG changeset patch
# User blanchet
# Date 1280769315 -7200
# Node ID e5978befb9510467a844c56f4acf9d2669220263
# Parent  ab528533db92eff6256e21fc04e2f6a007abf998
careful about which linear inductive predicates should be starred

diff -r ab528533db92 -r e5978befb951 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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