# HG changeset patch
# User blanchet
# Date 1291712332 -3600
# Node ID ec2734f34d0f49645bd1a766b2ab96c3f19063d3
# Parent  a4a5a465da8df4d4fc4c89dc719f9ed256496f03
make SML/NJ happy

diff -r a4a5a465da8d -r ec2734f34d0f src/HOL/Tools/SMT/smt_solver.ML
--- 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