# HG changeset patch
# User webertj
# Date 1259706586 0
# Node ID b5ca587d088555decf30175b97422896c53fb7a0
# Parent  6e77ca6d3a8f8293d6799f1d319166481c36cb8e
read_dimacs_cnf_file can now read DIMACS files that contain successive
white-space characters.

diff -r 6e77ca6d3a8f -r b5ca587d0885 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Sun Nov 29 12:56:30 2009 +1100
+++ b/src/HOL/Tools/sat_solver.ML	Tue Dec 01 22:29:46 2009 +0000
@@ -311,7 +311,7 @@
     fun int_from_string s =
       case Int.fromString s of
         SOME i => i
-      | NONE   => error ("token " ^ quote s ^ "in DIMACS CNF file is not a number")
+      | NONE   => error ("token " ^ quote s ^ " in DIMACS CNF file is not a number")
     (* int list -> int list list *)
     fun clauses xs =
       let
@@ -350,7 +350,7 @@
     o (map (map literal_from_int))
     o clauses
     o (map int_from_string)
-    o (maps (String.fields (fn c => c mem [#" ", #"\t", #"\n"])))
+    o (maps (String.tokens (fn c => c mem [#" ", #"\t", #"\n"])))
     o filter_preamble
     o filter (fn l => l <> "")
     o split_lines