--- 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: " ^