src/HOL/Matrix/cplex/Cplex_tools.ML
changeset 17521 0f1c48de39f5
parent 17412 e26cb20ef0cc
child 21056 2cfe839e8d58
     1.1 --- a/src/HOL/Matrix/cplex/Cplex_tools.ML	Tue Sep 20 15:12:40 2005 +0200
     1.2 +++ b/src/HOL/Matrix/cplex/Cplex_tools.ML	Tue Sep 20 16:17:34 2005 +0200
     1.3 @@ -969,10 +969,10 @@
     1.4  	val header = readHeader () 
     1.5  
     1.6  	val result = 
     1.7 -	    case assoc (header, "STATUS") of
     1.8 +	    case AList.lookup (op =) header "STATUS" of
     1.9  		SOME "INFEASIBLE" => Infeasible
    1.10  	      | SOME "UNBOUNDED" => Unbounded
    1.11 -	      | SOME "OPTIMAL" => Optimal (the (assoc (header, "OBJECTIVE")), 
    1.12 +	      | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"), 
    1.13  					   (skip_until_sep (); 
    1.14  					    skip_until_sep ();
    1.15  					    load_values ()))
    1.16 @@ -1118,10 +1118,10 @@
    1.17  	val header = readHeader ()
    1.18  
    1.19  	val result = 
    1.20 -	    case assoc (header, "STATUS") of
    1.21 +	    case AList.lookup (op =) header "STATUS" of
    1.22  		SOME "INFEASIBLE" => Infeasible
    1.23  	      | SOME "NONOPTIMAL" => Unbounded
    1.24 -	      | SOME "OPTIMAL" => Optimal (the (assoc (header, "OBJECTIVE")), 
    1.25 +	      | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"), 
    1.26  					   (skip_paragraph (); 
    1.27  					    skip_paragraph (); 
    1.28  					    skip_paragraph ();