changeset 41497 | 3fd79c771ed2 |
parent 41472 | f6ab14e61604 |
child 41601 | fda8511006f9 |
--- a/src/HOL/Tools/SMT/smt_solver.ML Mon Jan 10 17:37:11 2011 +0100 +++ b/src/HOL/Tools/SMT/smt_solver.ML Mon Jan 10 17:39:54 2011 +0100 @@ -175,8 +175,6 @@ val empty = Symtab.empty val extend = I fun merge data = Symtab.merge (K true) data - handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name) - (* FIXME never happens because of (K true) *) ) local