1.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Wed Aug 24 11:17:33 2011 +0200
     1.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Wed Aug 24 11:17:33 2011 +0200
     1.3 @@ -7,16 +7,22 @@
     1.4  
     1.5  signature SLEDGEHAMMER_TACTICS =
     1.6  sig
     1.7 +  type relevance_override = Sledgehammer_Filter.relevance_override
     1.8 +
     1.9    val sledgehammer_with_metis_tac :
    1.10 -    Proof.context -> (string * string) list -> int -> tactic
    1.11 +    Proof.context -> (string * string) list -> relevance_override -> int
    1.12 +    -> tactic
    1.13    val sledgehammer_as_oracle_tac :
    1.14 -    Proof.context -> (string * string) list -> int -> tactic
    1.15 +    Proof.context -> (string * string) list -> relevance_override -> int
    1.16 +    -> tactic
    1.17  end;
    1.18  
    1.19  structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
    1.20  struct
    1.21  
    1.22 -fun run_atp override_params i n ctxt goal =
    1.23 +open Sledgehammer_Filter
    1.24 +
    1.25 +fun run_atp override_params relevance_override i n ctxt goal =
    1.26    let
    1.27      val chained_ths = [] (* a tactic has no chained ths *)
    1.28      val params as {provers, relevance_thresholds, max_relevant, slicing, ...} =
    1.29 @@ -30,7 +36,6 @@
    1.30        Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
    1.31      val relevance_fudge =
    1.32        Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
    1.33 -    val relevance_override = {add = [], del = [], only = false}
    1.34      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
    1.35      val facts =
    1.36        Sledgehammer_Filter.nearly_all_facts ctxt relevance_override chained_ths
    1.37 @@ -62,16 +67,17 @@
    1.38      |> Source.exhaust
    1.39    end
    1.40  
    1.41 -fun sledgehammer_with_metis_tac ctxt override_params i th =
    1.42 -  case run_atp override_params i i ctxt th of
    1.43 +fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
    1.44 +  case run_atp override_params relevance_override i i ctxt th of
    1.45      SOME facts =>
    1.46      Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
    1.47    | NONE => Seq.empty
    1.48  
    1.49 -fun sledgehammer_as_oracle_tac ctxt override_params i th =
    1.50 +fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
    1.51    let
    1.52      val thy = Proof_Context.theory_of ctxt
    1.53 -    val xs = run_atp (override_params @ [("sound", "true")]) i i ctxt th
    1.54 +    val xs = run_atp (override_params @ [("sound", "true")]) relevance_override
    1.55 +                     i i ctxt th
    1.56    in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
    1.57  
    1.58  end;