# HG changeset patch
# User blanchet
# Date 1288879184 -3600
# Node ID 8fe3c26c49aff9d8f9f9a182681208549e4ef061
# Parent  14456fd302f071a56d6e0f3f792d5f957d71672e
ignore facts with only theory constants in them

diff -r 14456fd302f0 -r 8fe3c26c49af src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Nov 04 14:59:44 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Nov 04 14:59:44 2010 +0100
@@ -366,15 +366,19 @@
                    ||> filter_out (pconst_hyper_mem swap relevant_consts) of
     ([], _) => 0.0
   | (rel, irrel) =>
-    let
-      val irrel = irrel |> filter_out (pconst_mem swap rel)
-      val rel_weight =
-        0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
-      val irrel_weight =
-        ~ (locality_bonus fudge loc)
-        |> fold (curry (op +) o irrel_pconst_weight fudge const_tab) irrel
-      val res = rel_weight / (rel_weight + irrel_weight)
-    in if Real.isFinite res then res else 0.0 end
+    if forall (forall (String.isSuffix theory_const_suffix o fst))
+              [rel, irrel] then
+      0.0
+    else
+      let
+        val irrel = irrel |> filter_out (pconst_mem swap rel)
+        val rel_weight =
+          0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
+        val irrel_weight =
+          ~ (locality_bonus fudge loc)
+          |> fold (curry (op +) o irrel_pconst_weight fudge const_tab) irrel
+        val res = rel_weight / (rel_weight + irrel_weight)
+      in if Real.isFinite res then res else 0.0 end
 
 fun pconsts_in_fact thy is_built_in_const t =
   Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)