src/HOL/Matrix_LP/Cplex_tools.ML
changeset 51930 52fd62618631
parent 50902 cb2b940e2fdf
child 51940 958d439b3013
     1.1 --- a/src/HOL/Matrix_LP/Cplex_tools.ML	Sat May 11 16:13:08 2013 +0200
     1.2 +++ b/src/HOL/Matrix_LP/Cplex_tools.ML	Sat May 11 16:57:18 2013 +0200
     1.3 @@ -973,7 +973,7 @@
     1.4      result
     1.5      end
     1.6      handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
     1.7 -     | Option => raise (Load_cplexResult "Option")
     1.8 +     | Option.Option => raise (Load_cplexResult "Option")
     1.9  
    1.10  fun load_cplexResult name =
    1.11      let
    1.12 @@ -1122,7 +1122,7 @@
    1.13      result
    1.14      end
    1.15      handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
    1.16 -     | Option => raise (Load_cplexResult "Option")
    1.17 +     | Option.Option => raise (Load_cplexResult "Option")
    1.18  
    1.19  exception Execute of string;
    1.20