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,13 +1374,18 @@
     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 aux (Const (@{const_name Meson.skolem}, _) $ _) = I
     1.8 -      | aux (t $ u) = aux t #> aux u
     1.9 -      | aux (Const x) =
    1.10 -        fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
    1.11 -      | aux (Abs (_, _, u)) = aux u
    1.12 -      | aux _ = I
    1.13 -  in aux end
    1.14 +    fun add ((t as Const (s, _)) $ u) =
    1.15 +        if s = @{const_name Meson.skolem} orelse
    1.16 +           String.isPrefix skolem_const_prefix s then
    1.17 +          I
    1.18 +        else
    1.19 +          add t #> add u
    1.20 +      | add (t $ u) = add t #> add u
    1.21 +      | add (Const x) =
    1.22 +        x |> Sign.const_typargs thy |> fold (fold_type_consts set_insert)
    1.23 +      | add (Abs (_, _, u)) = add u
    1.24 +      | add _ = I
    1.25 +  in add end
    1.26  
    1.27  fun type_consts_of_terms thy ts =
    1.28    Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty)