src/HOL/SMT/Tools/smt_translate.ML

 local
   val dest_nat = (fn
       SApp (SConst (@{const_name nat}, _), [SApp (SNum (i, _), _)]) => SOME i
     | _ => NONE)
 in
-fun bv_rotate mk_name T ts =
+fun bv_rotate mk_name _ ts =
   dest_nat (hd ts) |> Option.map (fn i => (mk_name i, tl ts))
 
 fun bv_extend mk_name T ts =
   (case (try dest_wordT (domain_type T), try dest_wordT (range_type T)) of
     (SOME i, SOME j) => if j - i >= 0 then SOME (mk_name (j - i), ts) else NONE

     | @{const_name Ex} => SOME SExists
     | _ => NONE)
 
   fun group_quant qname vs (t as Const (q, _) $ Abs (n, T, u)) =
         if q = qname then group_quant qname ((n, T) :: vs) u else (vs, t)
-    | group_quant qname vs t = (vs, t)
+    | group_quant _ vs t = (vs, t)
 
   fun dest_trigger (@{term trigger} $ tl $ t) = (HOLogic.dest_list tl, t)
     | dest_trigger t = ([], t)
 
   fun pat f ts (Const (@{const_name pat}, _) $ t) = SPat (rev (f t :: ts))

     | pat f ts (Const (@{const_name andpat}, _) $ p $ t) = pat f (f t :: ts) p
     | pat _ _ t = raise TERM ("pat", [t])
 
   fun trans Ts t =
     (case Term.strip_comb t of
-      (t1 as Const (qn, qT), [t2 as Abs (n, T, t3)]) =>
+      (Const (qn, _), [Abs (n, T, t1)]) =>
         (case quantifier qn of
           SOME q =>
             let
-              val (vs, u) = group_quant qn [(n, T)] t3
+              val (vs, u) = group_quant qn [(n, T)] t1
               val Us = map snd vs @ Ts
               val (ps, b) = dest_trigger u
             in SQuant (q, rev vs, map (pat (trans Us) []) ps, trans Us b) end
         | NONE => raise TERM ("intermediate", [t]))
     | (Const (@{const_name Let}, _), [t1, Abs (n, T, t2)]) =>

     | SQuant (_, vs, _, u) => get_loc loc (i + length vs) u)
   and get_locs loc i ts = fold (either o get_loc loc i) ts NONE
 
   fun sep loc t =
     (case t of
-      SVar i => pair t
+      SVar _ => pair t
     | SApp (c as SConst (@{const_name If}, _), u :: us) =>
         mark sep false u ##>> fold_map (sep loc) us #>> app c o (op ::)
     | SApp (c, us) =>
         if not loc andalso member (op =) connectives c
         then fold_map (sep loc) us #>> app c

       SOME n => (n, st)
     | NONE =>
         let val (n, ns') = fresh_typ ns
         in (n, (vars, ns', add_typ (T, n) sgn)) end)
 
-  fun rep_var bs (n, T) (vars, ns, sgn) =
+  fun rep_var bs (_, T) (vars, ns, sgn) =
     let val (n', vars') = fresh_name vars
     in (vars', ns, sgn) |> rep_typ bs T |>> pair n' end
 
   fun rep_fun bs loc t T i (st as (_, _, sgn0)) =
     (case lookup_fun loc sgn0 t of

     val {builtin_fun, ...} = builtins
 
     fun sign loc t =
       (case t of
         SVar i => pair (SVar i)
-      | SApp (c as SConst (@{const_name term}, _), [u]) =>
+      | SApp (SConst (@{const_name term}, _), [u]) =>
           sign true u #>> app term_marker o single
-      | SApp (c as SConst (@{const_name formula}, _), [u]) =>
+      | SApp (SConst (@{const_name formula}, _), [u]) =>
           sign false u #>> app formula_marker o single
       | SApp (SConst (c as (_, T)), ts) =>
           (case builtin_lookup (builtin_fun loc) thy c ts of
             SOME (n, ts') => fold_map (sign loc) ts' #>> app n
           | NONE =>