src/HOL/Matrix_LP/Cplex_tools.ML
changeset 67405 e9ab4ad7bd15
parent 67399 eab6ce8368fa
child 76882 d9913b41a7bc
--- a/src/HOL/Matrix_LP/Cplex_tools.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Matrix_LP/Cplex_tools.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -969,10 +969,10 @@
     val header = readHeader ()
 
     val result =
-        case AList.lookup (=) header "STATUS" of
+        case AList.lookup (op =) header "STATUS" of
         SOME "INFEASIBLE" => Infeasible
           | SOME "UNBOUNDED" => Unbounded
-          | SOME "OPTIMAL" => Optimal (the (AList.lookup (=) header "OBJECTIVE"),
+          | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
                        (skip_until_sep ();
                         skip_until_sep ();
                         load_values ()))
@@ -1115,10 +1115,10 @@
     val header = readHeader ()
 
     val result =
-        case AList.lookup (=) header "STATUS" of
+        case AList.lookup (op =) header "STATUS" of
         SOME "INFEASIBLE" => Infeasible
           | SOME "NONOPTIMAL" => Unbounded
-          | SOME "OPTIMAL" => Optimal (the (AList.lookup (=) header "OBJECTIVE"),
+          | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
                        (skip_paragraph ();
                         skip_paragraph ();
                         skip_paragraph ();