# HG changeset patch # User wenzelm # Date 1186087427 -7200 # Node ID e7fb7ef2a85e336d682af03fa415a71104a5fdba # Parent 6e69e0031f349691a9b3bd5ffda95da1384f45ba added int type constraints to accomodate hacked SML/NJ; diff -r 6e69e0031f34 -r e7fb7ef2a85e src/HOL/Matrix/cplex/fspmlp.ML --- a/src/HOL/Matrix/cplex/fspmlp.ML Thu Aug 02 22:16:49 2007 +0200 +++ b/src/HOL/Matrix/cplex/fspmlp.ML Thu Aug 02 22:43:47 2007 +0200 @@ -41,7 +41,7 @@ datatype bound_type = LOWER | UPPER -fun intbound_ord ((i1, b1),(i2,b2)) = +fun intbound_ord ((i1: int, b1),(i2,b2)) = if i1 < i2 then LESS else if i1 = i2 then (if b1 = b2 then EQUAL else if b1=LOWER then LESS else GREATER)