1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 12:07:52 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 12:08:48 2010 +0200
     1.3 @@ -88,10 +88,11 @@
     1.4    Symtab.map_default (c, [ctyps])
     1.5                       (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
     1.6  
     1.7 -val fresh_sko_prefix = "Sledgehammer.Skox."
     1.8 +val fresh_prefix = "Sledgehammer.Fresh."
     1.9  
    1.10  val flip = Option.map not
    1.11  
    1.12 +val boring_natural_consts = [@{const_name If}]
    1.13  (* Including equality in this list might be expected to stop rules like
    1.14     subset_antisym from being chosen, but for some reason filtering works better
    1.15     with them listed. The logical signs All, Ex, &, and --> are omitted for CNF
    1.16 @@ -113,12 +114,15 @@
    1.17        | Free x => add_const_type_to_table (const_with_typ thy x)
    1.18        | (t as Const (@{const_name skolem_id}, _)) $ _ => do_term t
    1.19        | t1 $ t2 => do_term t1 #> do_term t2
    1.20 -      | Abs (_, _, t) => do_term t
    1.21 +      | Abs (_, _, t) =>
    1.22 +        (* Abstractions lead to combinators, so we add a penalty for them. *)
    1.23 +        add_const_type_to_table (gensym fresh_prefix, [])
    1.24 +        #> do_term t
    1.25        | _ => I
    1.26      fun do_quantifier sweet_pos pos body_t =
    1.27        do_formula pos body_t
    1.28        #> (if pos = SOME sweet_pos then I
    1.29 -          else add_const_type_to_table (gensym fresh_sko_prefix, []))
    1.30 +          else add_const_type_to_table (gensym fresh_prefix, []))
    1.31      and do_equality T t1 t2 =
    1.32        fold (if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE
    1.33              else do_term) [t1, t2]
    1.34 @@ -148,7 +152,8 @@
    1.35    in
    1.36      Symtab.empty
    1.37      |> (if !use_natural_form then
    1.38 -          fold (do_formula pos) ts
    1.39 +          fold (Symtab.update o rpair []) boring_natural_consts
    1.40 +          #> fold (do_formula pos) ts
    1.41          else
    1.42            fold (Symtab.update o rpair []) boring_cnf_consts
    1.43            #> fold do_term ts)
    1.44 @@ -361,9 +366,15 @@
    1.45        val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
    1.46                             Symtab.empty
    1.47        val goal_const_tab = get_consts_typs thy (SOME true) goals
    1.48 +      val relevance_threshold =
    1.49 +        if !use_natural_form then 0.9 * relevance_threshold (* experimental *)
    1.50 +        else relevance_threshold
    1.51        val _ =
    1.52          trace_msg (fn () => "Initial constants: " ^
    1.53 -                            commas (Symtab.keys goal_const_tab))
    1.54 +                            commas (goal_const_tab
    1.55 +                                    |> Symtab.dest
    1.56 +                                    |> filter (curry (op <>) [] o snd)
    1.57 +                                    |> map fst))
    1.58        val relevant =
    1.59          relevant_clauses ctxt relevance_convergence defs_relevant max_new
    1.60                           relevance_override const_tab relevance_threshold