src/HOL/Tools/SMT/smt_solver.ML

   val is_locally_installed: Proof.context -> string -> bool
   val is_remotely_available: Proof.context -> string -> bool
   val default_max_relevant: Proof.context -> string -> int
 
   (*filter*)
-  type 'a smt_filter_head_result = 'a list * (int option * thm) list *
+  type 'a smt_filter_head_result = ('a list * (int option * thm) list) *
     (((int * thm) list * Proof.context) * (int * (int option * thm)) list)
   val smt_filter_head: Proof.state ->
     ('a * (int option * thm)) list -> int -> 'a smt_filter_head_result
   val smt_filter_tail: Time.time -> bool -> 'a smt_filter_head_result ->
     {outcome: SMT_Failure.failure option, used_facts: ('a * thm) list}

 
 val cnot = Thm.cterm_of @{theory} @{const Not}
 
 fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules }
 
-type 'a smt_filter_head_result = 'a list * (int option * thm) list *
+type 'a smt_filter_head_result = ('a list * (int option * thm) list) *
   (((int * thm) list * Proof.context) * (int * (int option * thm)) list)
 
 fun smt_filter_head st xwrules i =
   let
     val ctxt =

     fun negate ct = Thm.dest_comb ct ||> Thm.capply cnot |-> Thm.capply
     val cprop = negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl))
 
     val (xs, wthms) = split_list xwrules
   in
-    (xs, wthms,
+    ((xs, wthms),
      wthms
      |> map_index I
      |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts))
      |> tap check_topsort
      |> `(gen_solver_head ctxt'))
   end
 
 fun smt_filter_tail time_limit run_remote
-    (xs, wthms, ((iwthms', ctxt), iwthms)) =
+    ((xs, wthms), ((iwthms', ctxt), iwthms)) =
   let
     val ctxt = ctxt |> Config.put C.timeout (Time.toReal time_limit)
     val xrules = xs ~~ map snd wthms
   in
     ((iwthms', ctxt), iwthms)