# HG changeset patch
# User haftmann
# Date 1259772824 -3600
# Node ID ab87cceed53fda6f7d56de6878a8a75f8e2f75fd
# Parent  b5ca587d088555decf30175b97422896c53fb7a0# Parent  f31d645b4e0095eea248e6f946b339b5420b9ca4
merged

diff -r f31d645b4e00 -r ab87cceed53f src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Wed Dec 02 17:53:36 2009 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Wed Dec 02 17:53:44 2009 +0100
@@ -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