# HG changeset patch
# User blanchet
# Date 1277219401 -7200
# Node ID 4308d2bbbca8aca16b76608d445b1bc2c43f28d4
# Parent  c2dfa26b9da637db3c16a46f636f6ba95055bb3e
more cosmetics

diff -r c2dfa26b9da6 -r 4308d2bbbca8 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 22 17:07:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 22 17:10:01 2010 +0200
@@ -441,16 +441,16 @@
 fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
   | fold_type_consts _ _ x = x;
 
-val add_type_consts_in_type = fold_type_consts setinsert;
-
 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
 fun add_type_consts_in_term thy =
-  let val const_typargs = Sign.const_typargs thy
-      fun add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x
-        | add_tcs (Abs (_, _, u)) x = add_tcs u x
-        | add_tcs (t $ u) x = add_tcs t (add_tcs u x)
-        | add_tcs _ x = x
-  in  add_tcs  end
+  let
+    val const_typargs = Sign.const_typargs thy
+    fun aux (Const cT) = fold (fold_type_consts setinsert) (const_typargs cT)
+      | aux (Abs (_, _, u)) = aux u
+      | aux (Const (@{const_name skolem_id}, _) $ _) = I
+      | aux (t $ u) = aux t #> aux u
+      | aux _ = I
+  in aux end
 
 fun type_consts_of_terms thy ts =
   Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);