--- a/src/HOL/Tools/SMT/smt_solver.ML Tue Dec 07 09:52:07 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Tue Dec 07 09:58:52 2010 +0100
@@ -216,7 +216,22 @@
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
@@ -235,21 +250,6 @@
|> 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