src/HOL/TPTP/sledgehammer_tactics.ML

--- a/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -7,14 +7,12 @@
 
 signature SLEDGEHAMMER_TACTICS =
 sig
-  type relevance_override = Sledgehammer_Fact.relevance_override
+  type fact_override = Sledgehammer_Fact.fact_override
 
   val sledgehammer_with_metis_tac :
-    Proof.context -> (string * string) list -> relevance_override -> int
-    -> tactic
+    Proof.context -> (string * string) list -> fact_override -> int -> tactic
   val sledgehammer_as_oracle_tac :
-    Proof.context -> (string * string) list -> relevance_override -> int
-    -> tactic
+    Proof.context -> (string * string) list -> fact_override -> int -> tactic
 end;
 
 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
@@ -22,10 +20,9 @@
 
 open Sledgehammer_Fact
 
-fun run_prover override_params relevance_override i n ctxt goal =
+fun run_prover override_params fact_override i n ctxt goal =
   let
     val mode = Sledgehammer_Provers.Normal
-    val chained_ths = [] (* a tactic has no chained ths *)
     val params as {provers, max_relevant, slice, ...} =
       Sledgehammer_Isar.default_params ctxt override_params
     val name = hd provers
@@ -35,11 +32,11 @@
     val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
     val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
     val facts =
-      Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override
-                                         chained_ths hyp_ts concl_t
+      Sledgehammer_Fact.nearly_all_facts ctxt ho_atp fact_override []
+                                         hyp_ts concl_t
       |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params name
-             (the_default default_max_relevant max_relevant) relevance_override
-             chained_ths hyp_ts concl_t
+             (the_default default_max_relevant max_relevant) fact_override
+             hyp_ts concl_t
     val problem =
       {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
        facts = facts |> map (apfst (apfst (fn name => name ())))
@@ -64,27 +61,23 @@
     |> Source.exhaust
   end
 
-fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
-  let
-    val override_params =
-      override_params @
-      [("preplay_timeout", "0")]
-  in
-    case run_prover override_params relevance_override i i ctxt th of
+fun sledgehammer_with_metis_tac ctxt override_params fact_override i th =
+  let val override_params = override_params @ [("preplay_timeout", "0")] in
+    case run_prover override_params fact_override i i ctxt th of
       SOME facts =>
       Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
           (maps (thms_of_name ctxt) facts) i th
     | NONE => Seq.empty
   end
 
-fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
+fun sledgehammer_as_oracle_tac ctxt override_params fact_override i th =
   let
     val thy = Proof_Context.theory_of ctxt
     val override_params =
       override_params @
       [("preplay_timeout", "0"),
        ("minimize", "false")]
-    val xs = run_prover override_params relevance_override i i ctxt th
+    val xs = run_prover override_params fact_override i i ctxt th
   in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
 
 end;