changeset 41472 | f6ab14e61604 |
parent 41432 | 3214c39777ab |
child 41497 | 3fd79c771ed2 |
--- a/src/HOL/Tools/SMT/smt_solver.ML Sat Jan 08 16:01:51 2011 +0100 +++ b/src/HOL/Tools/SMT/smt_solver.ML Sat Jan 08 17:14:48 2011 +0100 @@ -176,6 +176,7 @@ 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