src/HOL/SMT/Tools/z3_proof_terms.ML

 fun mk_bound thy i T =
   let val ct = Thm.cterm_of thy (Var ((Name.uu, 0), T))
   in mk_preterm (ct, [(i, ct)]) end
 
 local
-fun mk_quant q thy (n, T) e =
+fun mk_quant q thy (_, T) e =
   let
     val (ct, vs) = dest_preterm e
     val cv =
       (case AList.lookup (op =) vs 0 of
         SOME cv => cv