1.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Dec 07 09:52:07 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Dec 07 09:58:52 2010 +0100
     1.3 @@ -216,7 +216,22 @@
     1.4      else ()
     1.5    end
     1.6  
     1.7 -fun gen_solver name info rm ctxt irules =
     1.8 +
     1.9 +
    1.10 +(* registry *)
    1.11 +
    1.12 +type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm
    1.13 +
    1.14 +type solver_info = {
    1.15 +  env_var: string,
    1.16 +  is_remote: bool,
    1.17 +  options: Proof.context -> string list,
    1.18 +  interface: interface,
    1.19 +  reconstruct: string list * SMT_Translate.recon -> Proof.context ->
    1.20 +    (int list * thm) * Proof.context,
    1.21 +  default_max_relevant: int }
    1.22 +
    1.23 +fun gen_solver name (info : solver_info) rm ctxt irules =
    1.24    let
    1.25      val {env_var, is_remote, options, interface, reconstruct, ...} = info
    1.26      val {extra_norm, translate} = interface
    1.27 @@ -235,21 +250,6 @@
    1.28      |> pair idxs)
    1.29    end
    1.30  
    1.31 -
    1.32 -
    1.33 -(* registry *)
    1.34 -
    1.35 -type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm
    1.36 -
    1.37 -type solver_info = {
    1.38 -  env_var: string,
    1.39 -  is_remote: bool,
    1.40 -  options: Proof.context -> string list,
    1.41 -  interface: interface,
    1.42 -  reconstruct: string list * SMT_Translate.recon -> Proof.context ->
    1.43 -    (int list * thm) * Proof.context,
    1.44 -  default_max_relevant: int }
    1.45 -
    1.46  structure Solvers = Generic_Data
    1.47  (
    1.48    type T = solver_info Symtab.table