# HG changeset patch
# User blanchet
# Date 1284477796 -7200
# Node ID ce60294425a0fa05880dacf459e101854e230879
# Parent  f58fbb959826cefe9dcad212b231d7c2d6bcaf7f
tuning

diff -r f58fbb959826 -r ce60294425a0 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Sep 14 16:34:26 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Sep 14 17:23:16 2010 +0200
@@ -155,7 +155,7 @@
   case strip_comb t of
     (Const x, ts) => PApp (pconst thy true x ts)
   | (Free x, ts) => PApp (pconst thy false x ts)
-  | (Var x, []) => PVar
+  | (Var _, []) => PVar
   | _ => PApp ("?", [])  (* equivalence class of higher-order constructs *)
 (* Pairs a constant with the list of its type instantiations. *)
 and ptype thy const x ts =
@@ -298,7 +298,7 @@
 
 (**** Actual Filtering Code ****)
 
-fun pow_int x 0 = 1.0
+fun pow_int _ 0 = 1.0
   | pow_int x 1 = x
   | pow_int x n = if n > 0 then x * pow_int x (n - 1) else pow_int x (n + 1) / x
 
@@ -314,7 +314,7 @@
 (* "log" seems best in practice. A constant function of one ignores the constant
    frequencies. Rare constants give more points if they are relevant than less
    rare ones. *)
-fun rel_weight_for order freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0)
+fun rel_weight_for _ freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0)
 
 (* Irrelevant constants are treated differently. We associate lower penalties to
    very rare constants and very common ones -- the former because they can't
@@ -491,7 +491,7 @@
                       hopeless_rejects hopeful_rejects)
             end
           | relevant candidates rejects
-                     (((ax as (((_, loc), th), axiom_consts)), cached_weight)
+                     (((ax as (((_, loc), _), axiom_consts)), cached_weight)
                       :: hopeful) =
             let
               val weight =
@@ -799,7 +799,7 @@
 (***************************************************************)
 
 fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant
-                   (relevance_override as {add, del, only}) chained_ths hyp_ts
+                   (relevance_override as {add, only, ...}) chained_ths hyp_ts
                    concl_t =
   let
     val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),