minor Library.option related modifications
authorwebertj
Fri Mar 11 16:56:48 2005 +0100 (2005-03-11)
changeset 156050c544d8b521f
parent 15604 6fb06b768f67
child 15606 95617b30514b
minor Library.option related modifications
src/HOL/Tools/sat_solver.ML
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Fri Mar 11 16:35:06 2005 +0100
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Fri Mar 11 16:56:48 2005 +0100
     1.3 @@ -27,7 +27,7 @@
     1.4  	(* generic interface *)
     1.5  	val solvers       : (string * solver) list ref
     1.6  	val add_solver    : string * solver -> unit
     1.7 -	val invoke_solver : string -> solver  (* exception OPTION *)
     1.8 +	val invoke_solver : string -> solver  (* exception Option *)
     1.9  end;
    1.10  
    1.11  structure SatSolver : SAT_SOLVER =
    1.12 @@ -186,14 +186,9 @@
    1.13  
    1.14  	fun parse_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) =
    1.15  	let
    1.16 -		(* 'a option -> 'a option *)
    1.17 -		fun option (SOME a) =
    1.18 -			SOME a
    1.19 -		  | option NONE =
    1.20 -			NONE
    1.21  		(* string -> int list *)
    1.22  		fun int_list_from_string s =
    1.23 -			List.mapPartial (option o Int.fromString) (space_explode " " s)
    1.24 +			List.mapPartial Int.fromString (space_explode " " s)
    1.25  		(* int list -> assignment *)
    1.26  		fun assignment_from_list [] i =
    1.27  			NONE  (* the SAT solver didn't provide a value for this variable *)
    1.28 @@ -336,7 +331,7 @@
    1.29  
    1.30  (* ------------------------------------------------------------------------- *)
    1.31  (* invoke_solver: returns the solver associated with the given 'name'        *)
    1.32 -(* Note: If no solver is associated with 'name', exception 'OPTION' will be  *)
    1.33 +(* Note: If no solver is associated with 'name', exception 'Option' will be  *)
    1.34  (*       raised.                                                             *)
    1.35  (* ------------------------------------------------------------------------- *)
    1.36