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