# HG changeset patch
# User wenzelm
# Date 1257702202 -3600
# Node ID a4c54218be62b2d778c975d458e38c736b948e88
# Parent  b2cb4da715f753edbc7c0d530f76842394e3a578
adapted Theory_Data;
handle Symtab.DUP during actual merge;

diff -r b2cb4da715f7 -r a4c54218be62 src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Sun Nov 08 18:42:57 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Sun Nov 08 18:43:22 2009 +0100
@@ -204,13 +204,12 @@
 type solver = Proof.context -> thm list -> thm
 type solver_info = Context.generic -> Pretty.T list
 
-structure Solvers = TheoryDataFun
+structure Solvers = Theory_Data
 (
   type T = ((Proof.context -> solver_config) * solver_info) Symtab.table
   val empty = Symtab.empty
-  val copy = I
   val extend = I
-  fun merge _ = Symtab.merge (K true)
+  fun merge data = Symtab.merge (K true) data
     handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name)
 )