src/HOL/Tools/sat_solver.ML

 				case Int.fromString s of
 				  SOME i => i
 				| NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
 			)
 			(* parse the "resolve_trace" file *)
-			(* int ref *)
 			val clause_offset = ref ~1
-			(* string list -> proof -> proof *)
-			fun process_tokens [] proof =
-				proof
-			  | process_tokens (tok::toks) (clause_table, empty_id) =
+			val clause_table  = ref (Inttab.empty : int list Inttab.table)
+			val empty_id      = ref ~1
+			(* string list -> unit *)
+			fun process_tokens [] =
+				()
+			  | process_tokens (tok::toks) =
 				if tok="CL:" then (
 					case toks of
 					  id::sep::ids =>
 						let
 							val _   = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".")
-							val _   = if empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".")
+							val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".")
 							val cid = int_from_string id
 							val _   = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
 							val rs  = map int_from_string ids
 						in
 							(* update clause table *)
-							(Inttab.update_new (cid, rs) clause_table, empty_id)
+							clause_table := Inttab.update_new (cid, rs) (!clause_table)
 								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.")
 						end
 					| _ =>
 						raise INVALID_PROOF "File format error: \"CL:\" followed by an insufficient number of tokens."
 				) else if tok="VAR:" then (
 					case toks of
 					  id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits =>
 						let
-							val _   = if empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".")
+							val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".")
 							(* set 'clause_offset' to the largest used clause ID *)
 							val _   = if !clause_offset = ~1 then clause_offset :=
-								(case Inttab.max_key clause_table of
+								(case Inttab.max_key (!clause_table) of
 								  SOME id => id
 								| NONE    => cnf_number_of_clauses (PropLogic.defcnf fm) - 1  (* the first clause ID is 0, not 1 *))
 								else
 									()
 							val vid = int_from_string id

 							(* we add '!clause_offset' to obtain the ID of the corresponding unit clause  *)
 							val vids = filter (not_equal vid) (map (fn l => l div 2) ls)
 							val rs   = aid :: map (fn v => !clause_offset + v) vids
 						in
 							(* update clause table *)
-							(Inttab.update_new (cid, rs) clause_table, empty_id)
+							clause_table := Inttab.update_new (cid, rs) (!clause_table)
 								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.")
 						end
 					| _ =>
 						raise INVALID_PROOF "File format error: \"VAR:\" followed by an insufficient number of tokens."
 				) else if tok="CONF:" then (
 					case toks of
 					  id::sep::ids =>
 						let
-							val _   = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified."
+							val _   = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified."
 							val cid = int_from_string id
 							val _   = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).")
 							val ls  = map int_from_string ids
 							(* the conflict clause must be resolved with the unit clauses *)
 							(* for its literals to obtain the empty clause                *)
 							val vids         = map (fn l => l div 2) ls
 							val rs           = cid :: map (fn v => !clause_offset + v) vids
-							val new_empty_id = getOpt (Inttab.max_key clause_table, !clause_offset) + 1
+							val new_empty_id = getOpt (Inttab.max_key (!clause_table), !clause_offset) + 1
 						in
 							(* update clause table and conflict id *)
-							(Inttab.update_new (new_empty_id, rs) clause_table, new_empty_id)
-								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined.")
+							clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table)
+								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined.");
+							empty_id     := new_empty_id
 						end
 					| _ =>
 						raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens."
 				) else
 					raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
-			(* string list -> proof -> proof *)
-			fun process_lines [] proof =
-				proof
-			  | process_lines (l::ls) proof =
-				process_lines ls (process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l) proof)
+			(* string list -> unit *)
+			fun process_lines [] =
+				()
+			  | process_lines (l::ls) = (
+					process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
+					process_lines ls
+				)
 			(* proof *)
-			val (clause_table, empty_id) = process_lines proof_lines (Inttab.empty, ~1)
-			val _                        = if empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
+			val _ = process_lines proof_lines
+			val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
 		in
-			SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id))
+			SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
 		end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
 	| result =>
 		result
 in
 	SatSolver.add_solver ("zchaff_with_proofs", zchaff_with_proofs)