--- a/src/HOL/SMT/Tools/smt_solver.ML Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML Sun Nov 08 16:30:41 2009 +0100
@@ -223,12 +223,13 @@
(* selected solver *)
-structure SelectedSolver = GenericDataFun
+structure SelectedSolver = Generic_Data
(
type T = serial * string
val empty = (serial (), no_solver)
val extend = I
- fun merge _ (sl1 as (s1, _), sl2 as (s2, _)) = if s1 > s2 then sl1 else sl2
+ fun merge (sl1 as (s1, _), sl2 as (s2, _)) =
+ if s1 > s2 then sl1 else sl2 (* FIXME depends on accidental load order !?! *)
)
val solver_name_of = snd o SelectedSolver.get