# HG changeset patch
# User boehmes
# Date 1294388787 -3600
# Node ID 272fe1f37b6577f0b554bec21acd520133bd3a27
# Parent  5bc117c382ec40f0de9ae6decc1edba7e364bf49
made SML/NJ happy

diff -r 5bc117c382ec -r 272fe1f37b65 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Thu Jan 06 17:40:38 2011 -0800
+++ b/src/HOL/Tools/SMT/smt_config.ML	Fri Jan 07 09:26:27 2011 +0100
@@ -138,7 +138,8 @@
 fun solver_options_of ctxt =
   let
     fun all_options NONE = []
-      | all_options (SOME ({options, ...}, opts)) = opts @ options ctxt
+      | all_options (SOME ({options, ...} : solver_info, opts)) =
+          opts @ options ctxt
   in solver_info_of (K []) all_options ctxt end
 
 val setup_solver =