src/HOL/Tools/SMT/smt_solver.ML

       tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
         (map (Display.pretty_thm ctxt) thms)))
     else ()
   end
 
-fun gen_solver name info rm ctxt irules =
+
+
+(* registry *)
+
+type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm
+
+type solver_info = {
+  env_var: string,
+  is_remote: bool,
+  options: Proof.context -> string list,
+  interface: interface,
+  reconstruct: string list * SMT_Translate.recon -> Proof.context ->
+    (int list * thm) * Proof.context,
+  default_max_relevant: int }
+
+fun gen_solver name (info : solver_info) rm ctxt irules =
   let
     val {env_var, is_remote, options, interface, reconstruct, ...} = info
     val {extra_norm, translate} = interface
     val (with_datatypes, translate') =
       set_has_datatypes (Config.get ctxt C.datatypes) translate

     |> singleton (ProofContext.export ctxt' ctxt)
     |> discharge_definitions
     |> tap (fn _ => trace_assumptions ctxt irules idxs)
     |> pair idxs)
   end
-
-
-
-(* registry *)
-
-type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm
-
-type solver_info = {
-  env_var: string,
-  is_remote: bool,
-  options: Proof.context -> string list,
-  interface: interface,
-  reconstruct: string list * SMT_Translate.recon -> Proof.context ->
-    (int list * thm) * Proof.context,
-  default_max_relevant: int }
 
 structure Solvers = Generic_Data
 (
   type T = solver_info Symtab.table
   val empty = Symtab.empty