Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/sat_solver.ML
changeset 43701 f91c3c899911
parent 41944 b97091ae583a
child 43850 7f2cbc713344 
--- 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)) =
isabelle