diff -r 71fdbffe3275 -r b426cbdb5a23 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Tue Jun 22 13:17:59 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Tue Jun 22 14:28:22 2010 +0200
@@ -21,9 +21,8 @@
   val cnf_rules_pairs:
     theory -> (string * thm) list -> (thm * (string * int)) list
   val saturate_skolem_cache: theory -> theory option
-  val use_skolem_cache: bool Unsynchronized.ref
+  val auto_saturate_skolem_cache: bool Unsynchronized.ref
     (* for emergency use where the Skolem cache causes problems *)
-  val strip_subgoal : thm -> int -> (string * typ) list * term list * term
   val neg_clausify: thm -> thm list
   val neg_conjecture_clauses:
     Proof.context -> thm -> int -> thm list list * (string * typ) list
@@ -133,7 +132,7 @@
       | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
       | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
       | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
-      | dec_sko t thx = thx
+      | dec_sko _ thx = thx
   in dec_sko (prop_of th) ([], thy) end
 
 fun mk_skolem_id t =
@@ -168,7 +167,7 @@
       | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
       | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
       | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
-      | dec_sko t defs = defs (*Do nothing otherwise*)
+      | dec_sko _ defs = defs
   in  dec_sko (prop_of th) []  end;
 
 
@@ -520,22 +519,11 @@
 
 end;
 
-val use_skolem_cache = Unsynchronized.ref true
-
-fun clause_cache_endtheory thy =
-  if !use_skolem_cache then saturate_skolem_cache thy else NONE
-
+val auto_saturate_skolem_cache = Unsynchronized.ref true
 
-(* The cache can be kept smaller by inspecting the prop of each thm. Can ignore
-   all that are quasi-lambda-free, but then the individual theory caches become
-   much bigger. *)
+fun conditionally_saturate_skolem_cache thy =
+  if !auto_saturate_skolem_cache then saturate_skolem_cache thy else NONE
 
-fun strip_subgoal goal i =
-  let
-    val (t, frees) = Logic.goal_params (prop_of goal) i
-    val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
-    val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
-  in (rev (map dest_Free frees), hyp_ts, concl_t) end
 
 (*** Converting a subgoal into negated conjecture clauses. ***)
 
@@ -574,7 +562,7 @@
 (** setup **)
 
 val setup =
-  perhaps saturate_skolem_cache
-  #> Theory.at_end clause_cache_endtheory
+  perhaps conditionally_saturate_skolem_cache
+  #> Theory.at_end conditionally_saturate_skolem_cache
 
 end;