src/HOL/Matrix_LP/Cplex_tools.ML
changeset 67399 eab6ce8368fa
parent 62505 9e2a65912111
child 67405 e9ab4ad7bd15
--- a/src/HOL/Matrix_LP/Cplex_tools.ML	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Matrix_LP/Cplex_tools.ML	Wed Jan 10 15:25:09 2018 +0100
@@ -969,10 +969,10 @@
     val header = readHeader ()
 
     val result =
-        case AList.lookup (op =) header "STATUS" of
+        case AList.lookup (=) header "STATUS" of
         SOME "INFEASIBLE" => Infeasible
           | SOME "UNBOUNDED" => Unbounded
-          | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
+          | SOME "OPTIMAL" => Optimal (the (AList.lookup (=) header "OBJECTIVE"),
                        (skip_until_sep ();
                         skip_until_sep ();
                         load_values ()))
@@ -1115,10 +1115,10 @@
     val header = readHeader ()
 
     val result =
-        case AList.lookup (op =) header "STATUS" of
+        case AList.lookup (=) header "STATUS" of
         SOME "INFEASIBLE" => Infeasible
           | SOME "NONOPTIMAL" => Unbounded
-          | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
+          | SOME "OPTIMAL" => Optimal (the (AList.lookup (=) header "OBJECTIVE"),
                        (skip_paragraph ();
                         skip_paragraph ();
                         skip_paragraph ();