src/HOL/Tools/Nitpick/nitpick_nut.ML
changeset 41047 9f1d3fcef1ca
parent 41046 f2e94005d283
child 41049 0edd245892ed
--- 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)), []) =>