--- 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) =