# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 0c36ae874fcc994b4b842f9b824806d8dbd2df29
# Parent  95bd1ef1331aa9599c361f7d08d6dc56e9784234
fixed detection of Skolem constants in type construction detection code

diff -r 95bd1ef1331a -r 0c36ae874fcc src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -1374,15 +1374,11 @@
 (*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