diff -r 1bf1e21d3136 -r 2cfd0777580f src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 16:12:41 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 17:49:18 2010 +0200
@@ -231,7 +231,7 @@
   in if Real.isFinite res then res else 0.0 end
 
 (*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
-fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys;
+fun add_expand_pairs (x, ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys
 
 fun consts_typs_of_term thy t =
   Symtab.fold add_expand_pairs (get_consts_typs thy (SOME true) [t]) []
@@ -488,9 +488,10 @@
    are omitted. *)
 fun is_dangerous_term full_types t =
   not full_types andalso
-  ((has_bound_or_var_of_type dangerous_types t andalso
-    has_bound_or_var_of_type dangerous_types (transform_elim_term t))
-   orelse is_exhaustive_finite t)
+  let val t = transform_elim_term t in
+    has_bound_or_var_of_type dangerous_types t orelse
+    is_exhaustive_finite t
+  end
 
 fun is_theorem_bad_for_atps full_types thm =
   let val t = prop_of thm in