# HG changeset patch
# User boehmes
# Date 1257753427 -3600
# Node ID b34511bbc121251640755ff0193fb94834aa4c0d
# Parent  d4e5f6a407795646e52110d3e72674e03c5731c3
made theory merge deterministic wrt. the selected solver

diff -r d4e5f6a40779 -r b34511bbc121 src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Sun Nov 08 21:01:08 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Mon Nov 09 08:57:07 2009 +0100
@@ -222,21 +222,20 @@
 
 (* selected solver *)
 
-structure SelectedSolver = Generic_Data
+structure Selected_Solver = Generic_Data
 (
-  type T = serial * string
-  val empty = (serial (), no_solver)
+  type T = string
+  val empty = no_solver
   val extend = I
-  fun merge (sl1 as (s1, _), sl2 as (s2, _)) =
-    if s1 > s2 then sl1 else sl2   (* FIXME depends on accidental load order !?! *)
+  fun merge (_, s) = s
 )
 
-val solver_name_of = snd o SelectedSolver.get
+val solver_name_of = Selected_Solver.get
 
 fun select_solver name gen =
   if is_none (lookup_solver (Context.theory_of gen) name)
   then error ("SMT solver not registered: " ^ quote name)
-  else SelectedSolver.map (K (serial (), name)) gen
+  else Selected_Solver.map (K name) gen
 
 fun raw_solver_of gen =
   (case lookup_solver (Context.theory_of gen) (solver_name_of gen) of