1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 17:13:38 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 17:26:14 2010 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5    val use_natural_form : bool Unsynchronized.ref
     1.6    val relevant_facts :
     1.7 -    bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
     1.8 +    bool -> real -> real -> bool -> int -> bool -> relevance_override
     1.9      -> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list
    1.10  end;
    1.11  
    1.12 @@ -24,6 +24,7 @@
    1.13  open Clausifier
    1.14  open Metis_Clauses
    1.15  
    1.16 +val respect_no_atp = true
    1.17  (* Experimental feature: Filter theorems in natural form or in CNF? *)
    1.18  val use_natural_form = Unsynchronized.ref false
    1.19  
    1.20 @@ -392,7 +393,7 @@
    1.21  val exists_sledgehammer_const =
    1.22    exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) o prop_of
    1.23  
    1.24 -fun all_name_thms_pairs respect_no_atp ctxt chained_ths =
    1.25 +fun all_name_thms_pairs ctxt chained_ths =
    1.26    let
    1.27      val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
    1.28      val local_facts = ProofContext.facts_of ctxt;
    1.29 @@ -436,7 +437,7 @@
    1.30  
    1.31  (* The single-name theorems go after the multiple-name ones, so that single
    1.32     names are preferred when both are available. *)
    1.33 -fun name_thm_pairs respect_no_atp ctxt name_thms_pairs =
    1.34 +fun name_thm_pairs ctxt respect_no_atp name_thms_pairs =
    1.35    let
    1.36      val (mults, singles) = List.partition is_multi name_thms_pairs
    1.37      val ps = [] |> fold add_names singles |> fold add_names mults
    1.38 @@ -447,7 +448,7 @@
    1.39                Display.string_of_thm_without_context th); false)
    1.40    | is_named _ = true
    1.41  fun checked_name_thm_pairs respect_no_atp ctxt =
    1.42 -  name_thm_pairs respect_no_atp ctxt
    1.43 +  name_thm_pairs ctxt respect_no_atp
    1.44    #> tap (fn ps => trace_msg
    1.45                          (fn () => ("Considering " ^ Int.toString (length ps) ^
    1.46                                     " theorems")))
    1.47 @@ -505,8 +506,8 @@
    1.48      (has_typed_var dangerous_types t orelse
    1.49       forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)))
    1.50  
    1.51 -fun relevant_facts full_types respect_no_atp relevance_threshold
    1.52 -                   relevance_convergence defs_relevant max_new theory_relevant
    1.53 +fun relevant_facts full_types relevance_threshold relevance_convergence
    1.54 +                   defs_relevant max_new theory_relevant
    1.55                     (relevance_override as {add, del, only})
    1.56                     (ctxt, (chained_ths, _)) goal_cls =
    1.57    let
    1.58 @@ -517,8 +518,7 @@
    1.59      val axioms =
    1.60        checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
    1.61            (map (name_thms_pair_from_ref ctxt chained_ths) add @
    1.62 -           (if only then []
    1.63 -            else all_name_thms_pairs respect_no_atp ctxt chained_ths))
    1.64 +           (if only then [] else all_name_thms_pairs ctxt chained_ths))
    1.65        |> cnf_rules_pairs thy
    1.66        |> not has_override ? make_unique
    1.67        |> filter (fn (cnf_thm, (_, orig_thm)) =>