--- a/src/HOL/Matrix/cplex/Cplex_tools.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Matrix/cplex/Cplex_tools.ML Tue Sep 20 16:17:34 2005 +0200
@@ -969,10 +969,10 @@
val header = readHeader ()
val result =
- case assoc (header, "STATUS") of
+ case AList.lookup (op =) header "STATUS" of
SOME "INFEASIBLE" => Infeasible
| SOME "UNBOUNDED" => Unbounded
- | SOME "OPTIMAL" => Optimal (the (assoc (header, "OBJECTIVE")),
+ | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
(skip_until_sep ();
skip_until_sep ();
load_values ()))
@@ -1118,10 +1118,10 @@
val header = readHeader ()
val result =
- case assoc (header, "STATUS") of
+ case AList.lookup (op =) header "STATUS" of
SOME "INFEASIBLE" => Infeasible
| SOME "NONOPTIMAL" => Unbounded
- | SOME "OPTIMAL" => Optimal (the (assoc (header, "OBJECTIVE")),
+ | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
(skip_paragraph ();
skip_paragraph ();
skip_paragraph ();