src/Provers/Arith/fast_lin_arith.ML

 (* ------------------------------------------------------------------------- *)
 (* Add together (in)equations.                                               *)
 (* ------------------------------------------------------------------------- *)
 
 fun add_ineq (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) =
-  let val l = map2 (op +) (l1,l2)
+  let val l = map2 (curry (op +)) l1 l2
   in Lineq(k1+k2,find_add_type(ty1,ty2),l,Added(just1,just2)) end;
 
 (* ------------------------------------------------------------------------- *)
 (* Elimination of variable between a single pair of (in)equations.           *)
 (* If they're both inequalities, 1st coefficient must be +ve, 2nd -ve.       *)

 fun mklineq n atoms =
   fn (item,k) =>
   let val (m,(lhs,i,rel,rhs,j,discrete)) = integ item
       val lhsa = map (coeff lhs) atoms
       and rhsa = map (coeff rhs) atoms
-      val diff = map2 (op -) (rhsa,lhsa)
+      val diff = map2 (curry (op -)) rhsa lhsa
       val c = i-j
       val just = Asm k
       fun lineq(c,le,cs,j) = Lineq(c,le,cs, if m=1 then j else Multiplied2(m,j))
   in case rel of
       "<="   => lineq(c,Le,diff,just)