diff -r f2e94005d283 -r 9f1d3fcef1ca src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Dec 07 11:56:01 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Dec 07 11:56:01 2010 +0100 @@ -55,7 +55,6 @@ Eq | Triad | Composition | - Product | Image | Apply | Lambda @@ -170,7 +169,6 @@ Eq | Triad | Composition | - Product | Image | Apply | Lambda @@ -235,7 +233,6 @@ | string_for_op2 Eq = "Eq" | string_for_op2 Triad = "Triad" | string_for_op2 Composition = "Composition" - | string_for_op2 Product = "Product" | string_for_op2 Image = "Image" | string_for_op2 Apply = "Apply" | string_for_op2 Lambda = "Lambda" @@ -528,8 +525,6 @@ Op1 (Closure, range_type T, Any, sub t1) | (Const (@{const_name rel_comp}, T), [t1, t2]) => Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2) - | (Const (@{const_name prod}, T), [t1, t2]) => - Op2 (Product, nth_range_type 2 T, Any, sub t1, sub t2) | (Const (@{const_name image}, T), [t1, t2]) => Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2) | (Const (x as (s as @{const_name Suc}, T)), []) =>