--- 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),