comment;

--- a/src/HOL/Tools/sat_solver.ML	Fri Jul 08 11:50:58 2011 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Fri Jul 08 13:59:54 2011 +0200
@@ -797,6 +797,7 @@
     SatSolver.UNSATISFIABLE NONE =>
     (let
       (* string list *)
+      (* FIXME File.tmp_path (!?) *)
       val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace"))
         handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
       fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) =