# HG changeset patch
# User boehmes
# Date 1259148577 -3600
# Node ID 395df8f652b6538d670bda08cfdea0e35f6f1e5b
# Parent  24b648ea483456a9ec87a8f29e9e61a767b90a87
more generic explosion of options (also accept newlines, etc.)

diff -r 24b648ea4834 -r 395df8f652b6 src/HOL/SMT/Tools/z3_solver.ML
--- a/src/HOL/SMT/Tools/z3_solver.ML	Wed Nov 25 12:28:29 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_solver.ML	Wed Nov 25 12:29:37 2009 +0100
@@ -22,10 +22,12 @@
 
 fun add xs ys = ys @ xs
 
+fun explode_options s = String.tokens (Symbol.is_ascii_blank o str) s
+
 fun get_options ctxt =
   ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false"]
   |> Config.get ctxt proofs ? add ["DISPLAY_PROOF=true", "PROOF_MODE=2"]
-  |> add (space_explode " " (Config.get ctxt options))
+  |> add (explode_options (Config.get ctxt options))
 
 fun pretty_config context = [
   Pretty.str ("With proofs: " ^