1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 00:49:38 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 01:03:08 2010 +0200
     1.3 @@ -101,7 +101,8 @@
     1.4    | string_for_super_pseudoconst (s, Tss) =
     1.5      s ^ "{" ^ commas (map string_for_pseudotypes Tss) ^ "}"
     1.6  
     1.7 -val skolem_prefix = "Sledgehammer."
     1.8 +val abs_prefix = "Sledgehammer.abs"
     1.9 +val skolem_prefix = "Sledgehammer.sko"
    1.10  
    1.11  (* Add a pseudoconstant to the table, but a [] entry means a standard
    1.12     connective, which we ignore.*)
    1.13 @@ -129,7 +130,8 @@
    1.14          Const x => add_pseudoconst_to_table also_skolems (pseudoconst_for thy x)
    1.15        | Free (s, _) => add_pseudoconst_to_table also_skolems (s, [])
    1.16        | t1 $ t2 => fold do_term [t1, t2]
    1.17 -      | Abs (_, _, t') => do_term t'  (* FIXME: add penalty? *)
    1.18 +      | Abs (_, _, t') =>
    1.19 +        do_term t' #> add_pseudoconst_to_table true (abs_prefix, [])
    1.20        | _ => I
    1.21      fun do_quantifier will_surely_be_skolemized body_t =
    1.22        do_formula pos body_t
    1.23 @@ -247,6 +249,7 @@
    1.24  val rel_weight = rel_log oo pseudoconst_freq match_pseudotypes
    1.25  fun irrel_weight const_tab (c as (s, _)) =
    1.26    if String.isPrefix skolem_prefix s then 1.0
    1.27 +  else if String.isPrefix abs_prefix s then 2.0
    1.28    else irrel_log (pseudoconst_freq (match_pseudotypes o swap) const_tab c)
    1.29  (* TODO: experiment
    1.30  fun irrel_weight _ _ = 1.0