src/HOL/Tools/Sledgehammer/meson_clausify.ML

              clausify (to_definitional_cnf_with_quantifiers thy nnf_th)
            | p => p)
     fun intr_imp ct th =
       Thm.instantiate ([], map (pairself (cterm_of @{theory}))
                                [(Var (("i", 1), @{typ nat}),
-                                 HOLogic.mk_number @{typ nat} ax_no)])
+                                 HOLogic.mk_nat ax_no)])
                       @{thm skolem_COMBK_D}
       RS Thm.implies_intr ct th
   in
     (opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0)
                         ##> (term_of #> HOLogic.dest_Trueprop