src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 48323 7b5f7ca25d17
parent 47909 5f1afeebafbc
child 52174 7fd0b5cfbb79
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -619,7 +619,7 @@
     1.4          make_fun_or_set true T T1 T2 T'
     1.5              (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
     1.6              (map (term_for_rep true seen T2 T2 R o single)
     1.7 -                 (batch_list (arity_of_rep R) js))
     1.8 +                 (chunk_list (arity_of_rep R) js))
     1.9        end
    1.10      and term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
    1.11          if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k