more cosmetics
authorblanchet
Tue, 22 Jun 2010 17:10:01 +0200
changeset 37504 4308d2bbbca8
parent 37503 c2dfa26b9da6
child 37505 d9af5c01dc4a
more cosmetics
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);