# HG changeset patch
# User blanchet
# Date 1282777388 -7200
# Node ID 0d2f7f0614d15ae1bdc396daaffeb7b9eec82d02
# Parent  69fea359d3f8cf24bf68ac601eb6fe02c1775ebb
add a penalty for lambda-abstractions;
the penalty will kick in only when the goal contains no lambdas, in which case Sledgehammer previously totally disallowed any higher-order construct; this was too drastic;
lambdas are dangerous because they rapidly lead to unsound proofs; e.g. COMBI_def COMBS_def not_Cons_self2 with explicit_apply

diff -r 69fea359d3f8 -r 0d2f7f0614d1 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 00:49:38 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 01:03:08 2010 +0200
@@ -101,7 +101,8 @@
   | string_for_super_pseudoconst (s, Tss) =
     s ^ "{" ^ commas (map string_for_pseudotypes Tss) ^ "}"
 
-val skolem_prefix = "Sledgehammer."
+val abs_prefix = "Sledgehammer.abs"
+val skolem_prefix = "Sledgehammer.sko"
 
 (* Add a pseudoconstant to the table, but a [] entry means a standard
    connective, which we ignore.*)
@@ -129,7 +130,8 @@
         Const x => add_pseudoconst_to_table also_skolems (pseudoconst_for thy x)
       | Free (s, _) => add_pseudoconst_to_table also_skolems (s, [])
       | t1 $ t2 => fold do_term [t1, t2]
-      | Abs (_, _, t') => do_term t'  (* FIXME: add penalty? *)
+      | Abs (_, _, t') =>
+        do_term t' #> add_pseudoconst_to_table true (abs_prefix, [])
       | _ => I
     fun do_quantifier will_surely_be_skolemized body_t =
       do_formula pos body_t
@@ -247,6 +249,7 @@
 val rel_weight = rel_log oo pseudoconst_freq match_pseudotypes
 fun irrel_weight const_tab (c as (s, _)) =
   if String.isPrefix skolem_prefix s then 1.0
+  else if String.isPrefix abs_prefix s then 2.0
   else irrel_log (pseudoconst_freq (match_pseudotypes o swap) const_tab c)
 (* TODO: experiment
 fun irrel_weight _ _ = 1.0