1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Nov 22 22:10:31 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Nov 23 13:22:40 2009 +0100
     1.3 @@ -1740,9 +1740,12 @@
     1.4        | do_lfp_def _ = false
     1.5    in do_lfp_def o strip_abs_body end
     1.6  
     1.7 -(* typ -> typ -> term -> term *)
     1.8 -fun ap_split tuple_T =
     1.9 -  HOLogic.mk_psplits (HOLogic.flat_tupleT_paths tuple_T) tuple_T
    1.10 +(* int -> int list list *)
    1.11 +fun n_ptuple_paths 0 = []
    1.12 +  | n_ptuple_paths 1 = []
    1.13 +  | n_ptuple_paths n = [] :: map (cons 2) (n_ptuple_paths (n - 1))
    1.14 +(* int -> typ -> typ -> term -> term *)
    1.15 +val ap_n_split = HOLogic.mk_psplits o n_ptuple_paths
    1.16  
    1.17  (* term -> term * term *)
    1.18  val linear_pred_base_and_step_rhss =
    1.19 @@ -1776,16 +1779,17 @@
    1.20                                 |> List.foldl s_disj @{const False} 
    1.21          in
    1.22            (list_abs (tl xs, incr_bv (~1, j, base_body))
    1.23 -           |> ap_split tuple_T bool_T,
    1.24 +           |> ap_n_split (length arg_Ts) tuple_T bool_T,
    1.25             Abs ("y", tuple_T, list_abs (tl xs, step_body)
    1.26 -                              |> ap_split tuple_T bool_T))
    1.27 +                              |> ap_n_split (length arg_Ts) tuple_T bool_T))
    1.28          end
    1.29        | aux t =
    1.30          raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
    1.31    in aux end
    1.32  
    1.33  (* extended_context -> styp -> term -> term *)
    1.34 -fun closed_linear_pred_const (ext_ctxt as {simp_table, ...}) (x as (s, T)) def =
    1.35 +fun starred_linear_pred_const (ext_ctxt as {simp_table, ...}) (x as (s, T))
    1.36 +                              def =
    1.37    let
    1.38      val j = maxidx_of_term def + 1
    1.39      val (outer, fp_app) = strip_abs def
    1.40 @@ -1832,7 +1836,7 @@
    1.41        unrolled_const (* already done *)
    1.42      else if not gfp andalso is_linear_inductive_pred_def def
    1.43           andalso star_linear_preds then
    1.44 -      closed_linear_pred_const ext_ctxt x def
    1.45 +      starred_linear_pred_const ext_ctxt x def
    1.46      else
    1.47        let
    1.48          val j = maxidx_of_term def + 1