1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     1.3 @@ -1374,15 +1374,11 @@
     1.4  (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
     1.5  fun add_type_consts_in_term thy =
     1.6    let
     1.7 -    fun add ((t as Const (s, _)) $ u) =
     1.8 -        if s = @{const_name Meson.skolem} orelse
     1.9 -           String.isPrefix skolem_const_prefix s then
    1.10 -          I
    1.11 -        else
    1.12 -          add t #> add u
    1.13 +    fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
    1.14        | add (t $ u) = add t #> add u
    1.15 -      | add (Const x) =
    1.16 -        x |> Sign.const_typargs thy |> fold (fold_type_consts set_insert)
    1.17 +      | add (Const (x as (s, _))) =
    1.18 +        if String.isPrefix skolem_const_prefix s then I
    1.19 +        else x |> Sign.const_typargs thy |> fold (fold_type_consts set_insert)
    1.20        | add (Abs (_, _, u)) = add u
    1.21        | add _ = I
    1.22    in add end