src/HOL/Tools/sat_solver.ML
changeset 15605 0c544d8b521f
parent 15570 8d8c70b41bab
child 16270 4280d6bbc1bb
--- a/src/HOL/Tools/sat_solver.ML	Fri Mar 11 16:35:06 2005 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Fri Mar 11 16:56:48 2005 +0100
@@ -27,7 +27,7 @@
 	(* generic interface *)
 	val solvers       : (string * solver) list ref
 	val add_solver    : string * solver -> unit
-	val invoke_solver : string -> solver  (* exception OPTION *)
+	val invoke_solver : string -> solver  (* exception Option *)
 end;
 
 structure SatSolver : SAT_SOLVER =
@@ -186,14 +186,9 @@
 
 	fun parse_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) =
 	let
-		(* 'a option -> 'a option *)
-		fun option (SOME a) =
-			SOME a
-		  | option NONE =
-			NONE
 		(* string -> int list *)
 		fun int_list_from_string s =
-			List.mapPartial (option o Int.fromString) (space_explode " " s)
+			List.mapPartial Int.fromString (space_explode " " s)
 		(* int list -> assignment *)
 		fun assignment_from_list [] i =
 			NONE  (* the SAT solver didn't provide a value for this variable *)
@@ -336,7 +331,7 @@
 
 (* ------------------------------------------------------------------------- *)
 (* invoke_solver: returns the solver associated with the given 'name'        *)
-(* Note: If no solver is associated with 'name', exception 'OPTION' will be  *)
+(* Note: If no solver is associated with 'name', exception 'Option' will be  *)
 (*       raised.                                                             *)
 (* ------------------------------------------------------------------------- *)