# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID cd3b7798ecc2e9351bc558923b5a7a2b09e08a5d
# Parent  283114859d6c79366db3312219bbf4c664199cae
don't stumble on Skolem names

diff -r 283114859d6c -r cd3b7798ecc2 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,13 +1374,18 @@
 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
 fun add_type_consts_in_term thy =
   let
-    fun aux (Const (@{const_name Meson.skolem}, _) $ _) = I
-      | aux (t $ u) = aux t #> aux u
-      | aux (Const x) =
-        fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
-      | aux (Abs (_, _, u)) = aux u
-      | aux _ = I
-  in aux end
+    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
+      | add (t $ u) = add t #> add u
+      | add (Const x) =
+        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 =
   Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty)