--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Jan 03 18:33:18 2012 +0100
@@ -1110,8 +1110,9 @@
Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)),
shape_tuple T2 R2 (List.drop (us, arity1))])
end
- | shape_tuple (T as Type (@{type_name fun}, [_, T2])) (R as Vect (k, R')) us =
- Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us))
+ | shape_tuple T (R as Vect (k, R')) us =
+ Tuple (T, R, map (shape_tuple (pseudo_range_type T) R')
+ (batch_list (length us div k) us))
| shape_tuple T _ [u] =
if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
| shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us)