src/HOL/Tools/SMT/smt_config.ML

--- a/src/HOL/Tools/SMT/smt_config.ML	Wed May 30 16:05:21 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML	Wed May 30 23:10:42 2012 +0200
@@ -9,7 +9,7 @@
   (*solver*)
   type solver_info = {
     name: string,
-    class: SMT_Utils.class,
+    class: Proof.context -> SMT_Utils.class,
     avail: unit -> bool,
     options: Proof.context -> string list }
   val add_solver: solver_info -> Context.generic -> Context.generic
@@ -61,7 +61,7 @@
 
 type solver_info = {
   name: string,
-  class: SMT_Utils.class,
+  class: Proof.context -> SMT_Utils.class,
   avail: unit -> bool,
   options: Proof.context -> string list }
 
@@ -131,7 +131,8 @@
   | (_, NONE) => default ())
 
 fun solver_class_of ctxt =
-  solver_info_of no_solver_err (#class o fst o the) ctxt
+  let fun class_of ({class, ...}: solver_info, _) = class ctxt
+  in solver_info_of no_solver_err (class_of o the) ctxt end
 
 fun solver_options_of ctxt =
   let