author | boehmes |
Mon, 10 Jan 2011 17:39:54 +0100 | |
changeset 41497 | 3fd79c771ed2 |
parent 41496 | b2c1cd0bbcb9 |
child 41498 | a45cfc6dfd10 |
--- 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