# HG changeset patch
# User boehmes
# Date 1294682334 -3600
# Node ID d54fe826250e55facdf0bfe64f12bbbd980188cc
# Parent  a45cfc6dfd107e48c3db94e2b4e49afa41a2ba7f
be more precise: also merge option values

diff -r a45cfc6dfd10 -r d54fe826250e src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Mon Jan 10 17:41:45 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Mon Jan 10 18:58:54 2011 +0100
@@ -68,7 +68,8 @@
   type T = (solver_info * string list) Symtab.table * string option
   val empty = (Symtab.empty, NONE)
   val extend = I
-  fun merge ((ss1, s), (ss2, _)) = (Symtab.merge (K true) (ss1, ss2), s (* FIXME merge options!? *))
+  fun merge ((ss1, s1), (ss2, s2)) =
+    (Symtab.merge (K true) (ss1, ss2), merge_options (s1, s2))
 )
 
 fun set_solver_options (name, options) =