# HG changeset patch
# User webertj
# Date 1110556608 -3600
# Node ID 0c544d8b521f2e2b7baef340719d00454fe9246f
# Parent  6fb06b768f678aecf1f9875bd47ded66b93b6621
minor Library.option related modifications

diff -r 6fb06b768f67 -r 0c544d8b521f src/HOL/Tools/sat_solver.ML
--- 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.                                                             *)
 (* ------------------------------------------------------------------------- *)