# HG changeset patch
# User blanchet
# Date 1281343193 -7200
# Node ID 7497c22bb185e0dff57a7f8d705738d4138858ec
# Parent  aee5862973e021670e2b834028e175ff6aa981d5
remove debugging output

diff -r aee5862973e0 -r 7497c22bb185 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 09 10:38:57 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 09 10:39:53 2010 +0200
@@ -312,7 +312,6 @@
                 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
@@ -557,7 +556,7 @@
     val thy = ProofContext.theory_of ctxt
     val add_thms = maps (ProofContext.get_fact ctxt) add
     val has_override = not (null add) orelse not (null del)
-(*###
+(* FIXME:
     val is_FO = forall Meson.is_fol_term thy (concl_t :: hyp_ts)
 *)
     val axioms =
@@ -567,7 +566,7 @@
       |> not has_override ? make_unique
       |> filter (fn (_, th) =>
                     member Thm.eq_thm add_thms th orelse
-                    ((* ### FIXME: keep? (not is_FO orelse is_quasi_fol_theorem thy th) andalso*)
+                    ((* FIXME: keep? (not is_FO orelse is_quasi_fol_theorem thy th) andalso*)
                      not (is_dangerous_term full_types (prop_of th))))
   in
     relevance_filter ctxt relevance_threshold relevance_convergence