src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 58634 9f10d82e8188
parent 56254 a2dd9200854d
child 58843 521cea5fa777
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Oct 08 14:34:30 2014 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Oct 08 17:09:07 2014 +0200
     1.3 @@ -508,7 +508,7 @@
     1.4            val k2 = k div k1
     1.5          in
     1.6            list_comb (HOLogic.pair_const T1 T2,
     1.7 -                     map3 (fn T => term_for_atom seen T T) [T1, T2]
     1.8 +                     @{map 3} (fn T => term_for_atom seen T T) [T1, T2]
     1.9                            (* ### k2 or k1? FIXME *)
    1.10                            [j div k2, j mod k2] [k1, k2])
    1.11          end
    1.12 @@ -578,7 +578,7 @@
    1.13                    if length arg_Ts = 0 then
    1.14                      []
    1.15                    else
    1.16 -                    map3 (fn Ts => term_for_rep true seen Ts Ts) arg_Ts arg_Rs
    1.17 +                    @{map 3} (fn Ts => term_for_rep true seen Ts Ts) arg_Ts arg_Rs
    1.18                           arg_jsss
    1.19                      |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
    1.20                      |> dest_n_tuple (length uncur_arg_Ts)
    1.21 @@ -633,7 +633,7 @@
    1.22            val (js1, js2) = chop arity1 js
    1.23          in
    1.24            list_comb (HOLogic.pair_const T1 T2,
    1.25 -                     map3 (fn T => term_for_rep true seen T T) [T1, T2] [R1, R2]
    1.26 +                     @{map 3} (fn T => term_for_rep true seen T T) [T1, T2] [R1, R2]
    1.27                            [[js1], [js2]])
    1.28          end
    1.29        | term_for_rep _ seen T T' (Vect (k, R')) [js] =