# HG changeset patch
# User wenzelm
# Date 1310126394 -7200
# Node ID f91c3c8999112ed0e771c921de5521bfe9057d43
# Parent  e4ece46a9ca70e701c67deab1a2ae93d9ad7f1a0
comment;

diff -r e4ece46a9ca7 -r f91c3c899911 src/HOL/Tools/sat_solver.ML
--- 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)) =