src/HOL/Tools/ATP/atp_translate.ML

   | fold_type_consts _ _ x = x
 
 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
 fun add_type_consts_in_term thy =
   let
-    fun add ((t as Const (s, _)) $ u) =
-        if s = @{const_name Meson.skolem} orelse
-           String.isPrefix skolem_const_prefix s then
-          I
-        else
-          add t #> add u
+    fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
       | add (t $ u) = add t #> add u
-      | add (Const x) =
-        x |> Sign.const_typargs thy |> fold (fold_type_consts set_insert)
+      | add (Const (x as (s, _))) =
+        if String.isPrefix skolem_const_prefix s then I
+        else x |> Sign.const_typargs thy |> fold (fold_type_consts set_insert)
       | add (Abs (_, _, u)) = add u
       | add _ = I
   in add end
 
 fun type_consts_of_terms thy ts =