src/HOL/Tools/refute.ML
changeset 25538 58e8ba3b792b
parent 25032 f7095d7cb9a3
child 26328 b2d6f520172c
--- a/src/HOL/Tools/refute.ML	Wed Dec 05 14:15:59 2007 +0100
+++ b/src/HOL/Tools/refute.ML	Wed Dec 05 14:16:05 2007 +0100
@@ -2181,7 +2181,7 @@
                   (* C_i x_1 ... x_n < C_i y_1 ... y_n if *)
                   (* (x_1, ..., x_n) < (y_1, ..., y_n)    *)
                   constructor_terms
-                    (map (op $) (Library.product terms d_terms)) ds
+                    (map_product (curry op $) terms d_terms) ds
                 end
             in
               (* C_i ... < C_j ... if i < j *)