# HG changeset patch
# User blanchet
# Date 1280437056 -7200
# Node ID 34b75b71235d0b2a405bee8fc667a665ad136a60
# Parent  e458a0dd3dc1b0624b8ba7a6550a63469eb6f23b
handle division by zero gracefully (used to raise Unordered later on)

diff -r e458a0dd3dc1 -r 34b75b71235d src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Jul 29 22:43:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Jul 29 22:57:36 2010 +0200
@@ -218,11 +218,11 @@
   but irrelevant constants are simply counted. Otherwise, Skolem functions,
   which are rare, would harm a formula's chances of being picked.*)
 fun formula_weight const_tab gctyps consts_typs =
-    let val rel = filter (uni_mem gctyps) consts_typs
-        val rel_weight = fold (curry Real.+ o ct_weight const_tab) rel 0.0
-    in
-        rel_weight / (rel_weight + real (length consts_typs - length rel))
-    end;
+  let
+    val rel = filter (uni_mem gctyps) consts_typs
+    val rel_weight = fold (curry Real.+ o ct_weight const_tab) rel 0.0
+    val res = rel_weight / (rel_weight + real (length consts_typs - length rel))
+  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;
@@ -312,6 +312,7 @@
                 if member Thm.eq_thm add_thms th then 1.0
                 else if member Thm.eq_thm del_thms th then 0.0
                 else formula_weight const_tab rel_const_tab consts_typs
+val _ = (if Real.isFinite weight then () else error ("*** " ^ Real.toString weight)) (*###*)
             in
               if weight >= threshold orelse
                  (defs_relevant andalso defines thy th rel_const_tab) then