author chaieb Tue, 12 Jun 2007 12:00:03 +0200 changeset 23341 985190a9bc39 parent 23340 57c6a46d9153 child 23342 0261d2da0b1c
turned curry (op opr) into curry op opr --- because of smlnj
```--- a/src/HOL/Tools/Presburger/cooper.ML	Tue Jun 12 11:01:16 2007 +0200
+++ b/src/HOL/Tools/Presburger/cooper.ML	Tue Jun 12 12:00:03 2007 +0200
@@ -179,10 +179,10 @@
| linear_cmul n tm =
case tm of
Const("HOL.plus_class.plus",_)\$a\$b => addC\$(linear_cmul n a)\$(linear_cmul n b)
-    | Const ("HOL.times_class.times",_)\$c\$x => mulC\$(numeral1 ((curry (op *)) n) c)\$x
+    | Const ("HOL.times_class.times",_)\$c\$x => mulC\$(numeral1 ((curry op *) n) c)\$x
| Const("HOL.minus_class.minus",_)\$a\$b => subC\$(linear_cmul n a)\$(linear_cmul n b)
| (m as Const("HOL.minus_class.uminus",_))\$a => m\$(linear_cmul n a)
-    | _ =>  numeral1 ((curry (op *)) n) tm;
+    | _ =>  numeral1 ((curry op *) n) tm;
fun earlier [] x y = false
| earlier (h::t) x y =
if h aconv y then false else if h aconv x then true else earlier t x y;
@@ -192,7 +192,7 @@
(Const("HOL.plus_class.plus",_)\$(Const("HOL.times_class.times",_)\$c1\$x1)\$r1,
Const("HOL.plus_class.plus",_)\$(Const("HOL.times_class.times",_)\$c2\$x2)\$r2) =>
if x1 = x2 then
-     let val c = numeral2 (curry (op +)) c1 c2
+     let val c = numeral2 (curry op +) c1 c2
in if c = zero then linear_add vars r1  r2