changeset 58634 | 9f10d82e8188 |
parent 57992 | 2371bff894f9 |
child 58843 | 521cea5fa777 |
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Oct 08 14:34:30 2014 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Oct 08 17:09:07 2014 +0200 @@ -1319,7 +1319,7 @@ construct_value ctxt (if new_s = @{type_name prod} then @{const_name Pair} else @{const_name PairBox}, new_Ts ---> new_T) - (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2] + (@{map 3} (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2] [t1, t2]) | t' => raise TERM ("Nitpick_HOL.coerce_term", [t']) else