# HG changeset patch
# User blanchet
# Date 1342593843 -7200
# Node ID 7fcee834c7f57e76c412a5db83d741a8dc91e453
# Parent  72129a5c1a8df42c1b67537c748e75c693da7a38
more code rationalization in relevance filter

diff -r 72129a5c1a8d -r 7fcee834c7f5 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -461,12 +461,11 @@
         val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name
         val facts =
           Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
-              Sledgehammer_Fact.no_relevance_override chained_ths hyp_ts concl_t
+              Sledgehammer_Fact.no_fact_override chained_ths hyp_ts concl_t
           |> filter (is_appropriate_prop o prop_of o snd)
           |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params prover_name
                  (the_default default_max_relevant max_relevant)
-                 Sledgehammer_Fact.no_relevance_override chained_ths hyp_ts
-                 concl_t
+                 Sledgehammer_Fact.no_fact_override hyp_ts concl_t
         val problem =
           {state = st', goal = goal, subgoal = i,
            subgoal_count = Sledgehammer_Util.subgoal_count st,
@@ -628,13 +627,13 @@
           #> fst
         val thms = named_thms |> maps snd
         val facts = named_thms |> map (ref_of_str o fst o fst)
-        val relevance_override = {add = facts, del = [], only = true}
+        val fact_override = {add = facts, del = [], only = true}
         fun my_timeout time_slice =
           timeout |> Time.toReal |> curry Real.* time_slice |> Time.fromReal
         fun sledge_tac time_slice prover type_enc =
           Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
-            (override_params prover type_enc (my_timeout time_slice))
-            relevance_override
+              (override_params prover type_enc (my_timeout time_slice))
+              fact_override
       in
         if !reconstructor = "sledgehammer_tac" then
           sledge_tac 0.2 ATP_Systems.z3_tptpN "mono_native"
diff -r 72129a5c1a8d -r 7fcee834c7f5 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -129,12 +129,11 @@
          val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
          val facts =
            Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
-               Sledgehammer_Fact.no_relevance_override chained_ths hyp_ts concl_t
+               Sledgehammer_Fact.no_fact_override chained_ths hyp_ts concl_t
            |> filter (is_appropriate_prop o prop_of o snd)
            |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
                   default_prover (the_default default_max_relevant max_relevant)
-                  (SOME relevance_fudge) Sledgehammer_Fact.no_relevance_override
-                  chained_ths hyp_ts concl_t
+                  (SOME relevance_fudge) hyp_ts concl_t
             |> map ((fn name => name ()) o fst o fst)
          val (found_facts, lost_facts) =
            flat proofs |> sort_distinct string_ord
diff -r 72129a5c1a8d -r 7fcee834c7f5 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -114,8 +114,9 @@
         val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
         val isa_facts = sugg_facts hyp_ts concl_t facts isa_deps
         val iter_facts =
-          iter_facts ctxt params (max_relevant_slack * the max_relevant) goal
-                     facts
+          Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
+              prover_name (max_relevant_slack * the max_relevant) NONE hyp_ts
+              concl_t facts
         val mash_facts = sugg_facts hyp_ts concl_t facts suggs
         val iter_mash_facts = hybrid_facts (iter_facts, mash_facts)
         val iter_s = prove iter_ok iterN iter_facts goal
diff -r 72129a5c1a8d -r 7fcee834c7f5 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -46,7 +46,8 @@
     val parents = parent_thms thy_ths thy
   in fold do_fact new_facts parents; () end
 
-fun generate_iter_suggestions ctxt params thy max_relevant file_name =
+fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant
+                              file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
@@ -58,14 +59,17 @@
       let
         val name = Thm.get_name_hint th
         val goal = goal_of_thm thy th
+        val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
         val kind = Thm.legacy_get_kind th
         val _ =
           if kind <> "" then
             let
               val suggs =
-                old_facts |> iter_facts ctxt params max_relevant goal
-                          |> map (fn ((name, _), _) => fact_name_of (name ()))
-                          |> sort string_ord
+                old_facts
+                |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
+                                (hd provers) max_relevant NONE hyp_ts concl_t
+                |> map (fn ((name, _), _) => fact_name_of (name ()))
+                |> sort string_ord
               val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n"
             in File.append path s end
           else
diff -r 72129a5c1a8d -r 7fcee834c7f5 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;
diff -r 72129a5c1a8d -r 7fcee834c7f5 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -10,14 +10,14 @@
   type status = ATP_Problem_Generate.status
   type stature = ATP_Problem_Generate.stature
 
-  type relevance_override =
+  type fact_override =
     {add : (Facts.ref * Attrib.src list) list,
      del : (Facts.ref * Attrib.src list) list,
      only : bool}
 
   val ignore_no_atp : bool Config.T
   val instantiate_inducts : bool Config.T
-  val no_relevance_override : relevance_override
+  val no_fact_override : fact_override
   val fact_from_ref :
     Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
     -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
@@ -32,7 +32,7 @@
     -> (((unit -> string) * stature) * thm) list
   val all_facts_of : theory -> (((unit -> string) * stature) * thm) list
   val nearly_all_facts :
-    Proof.context -> bool -> relevance_override -> thm list -> term list -> term
+    Proof.context -> bool -> fact_override -> thm list -> term list -> term
     -> (((unit -> string) * stature) * thm) list
 end;
 
@@ -43,7 +43,7 @@
 open Metis_Tactic
 open Sledgehammer_Util
 
-type relevance_override =
+type fact_override =
   {add : (Facts.ref * Attrib.src list) list,
    del : (Facts.ref * Attrib.src list) list,
    only : bool}
@@ -56,7 +56,7 @@
 val instantiate_inducts =
   Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
 
-val no_relevance_override = {add = [], del = [], only = false}
+val no_fact_override = {add = [], del = [], only = false}
 
 fun needs_quoting reserved s =
   Symtab.defined reserved s orelse
@@ -424,23 +424,27 @@
     |> rev (* try to restore the original order of facts, for MaSh *)
   end
 
-fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override)
-                     chained_ths hyp_ts concl_t =
+fun nearly_all_facts ctxt ho_atp {add, del, only} chained_ths hyp_ts concl_t =
   if only andalso null add then
     []
   else
     let
+      val chained_ths =
+        chained_ths
+        |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
       val reserved = reserved_isar_keyword_table ()
-      val add_ths = Attrib.eval_thms ctxt add
       val css_table = clasimpset_rule_table_of ctxt
     in
       (if only then
          maps (map (fn ((name, stature), th) => ((K name, stature), th))
                o fact_from_ref ctxt reserved chained_ths css_table) add
        else
-         all_facts ctxt ho_atp reserved false add_ths chained_ths css_table)
+         let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
+           all_facts ctxt ho_atp reserved false add chained_ths css_table
+           |> filter_out (member Thm.eq_thm_prop del o snd)
+           |> maybe_filter_no_atps ctxt
+         end)
       |> maybe_instantiate_inducts ctxt hyp_ts concl_t
-      |> not only ? maybe_filter_no_atps ctxt
       |> uniquify
     end
 
diff -r 72129a5c1a8d -r 7fcee834c7f5 src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -8,7 +8,6 @@
 signature SLEDGEHAMMER_FILTER_ITER =
 sig
   type stature = ATP_Problem_Generate.stature
-  type relevance_override = Sledgehammer_Fact.relevance_override
   type params = Sledgehammer_Provers.params
   type relevance_fudge = Sledgehammer_Provers.relevance_fudge
 
@@ -20,8 +19,7 @@
     -> string list
   val iterative_relevant_facts :
     Proof.context -> params -> string -> int -> relevance_fudge option
-    -> relevance_override -> thm list -> term list -> term
-    -> (((unit -> string) * stature) * thm) list
+    -> term list -> term -> (((unit -> string) * stature) * thm) list
     -> (((unit -> string) * stature) * thm) list
 end;
 
@@ -29,7 +27,6 @@
 struct
 
 open ATP_Problem_Generate
-open Sledgehammer_Fact
 open Sledgehammer_Provers
 
 val trace =
@@ -397,12 +394,15 @@
 val special_fact_index = 75
 
 fun relevance_filter ctxt thres0 decay max_relevant is_built_in_const
-        (fudge as {threshold_divisor, ridiculous_threshold, ...})
-        ({del, ...} : relevance_override) facts chained_ts hyp_ts concl_t =
+        (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts
+        concl_t =
   let
     val thy = Proof_Context.theory_of ctxt
     val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
     val add_pconsts = add_pconsts_in_term thy is_built_in_const false o SOME
+    val chained_ts =
+      facts |> map_filter (fn ((_, (Chained, _)), th) => SOME (prop_of th)
+                            | _ => NONE)
     val chained_const_tab = Symtab.empty |> fold (add_pconsts true) chained_ts
     val goal_const_tab =
       Symtab.empty |> fold (add_pconsts true) hyp_ts
@@ -410,8 +410,6 @@
       |> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
       |> fold (if_empty_replace_with_scope thy is_built_in_const facts)
               [Chained, Assum, Local]
-    val del_ths = Attrib.eval_thms ctxt del
-    val facts = facts |> filter_out (member Thm.eq_thm_prop del_ths o snd)
     fun iter j remaining_max thres rel_const_tab hopeless hopeful =
       let
         fun relevant [] _ [] =
@@ -515,7 +513,7 @@
 
 fun iterative_relevant_facts ctxt
         ({relevance_thresholds = (thres0, thres1), ...} : params) prover
-        max_relevant fudge override chained_ths hyp_ts concl_t facts =
+        max_relevant fudge hyp_ts concl_t facts =
   let
     val thy = Proof_Context.theory_of ctxt
     val is_built_in_const =
@@ -535,7 +533,7 @@
        []
      else
        relevance_filter ctxt thres0 decay max_relevant is_built_in_const
-           fudge override facts (chained_ths |> map prop_of) hyp_ts
+           fudge facts hyp_ts
            (concl_t |> theory_constify fudge (Context.theory_name thy)))
   end
 
diff -r 72129a5c1a8d -r 7fcee834c7f5 src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -9,7 +9,7 @@
   type status = ATP_Problem_Generate.status
   type stature = ATP_Problem_Generate.stature
   type params = Sledgehammer_Provers.params
-  type relevance_override = Sledgehammer_Fact.relevance_override
+  type fact_override = Sledgehammer_Fact.fact_override
   type relevance_fudge = Sledgehammer_Provers.relevance_fudge
   type prover_result = Sledgehammer_Provers.prover_result
 
@@ -24,10 +24,6 @@
   val features_of : theory -> status * thm -> string list
   val isabelle_dependencies_of : string list -> thm -> string list
   val goal_of_thm : theory -> thm -> thm
-  val iter_facts :
-    Proof.context -> params -> int -> thm
-    -> (((unit -> string) * stature) * thm) list
-    -> (((unit -> string) * stature) * thm) list
   val run_prover :
     Proof.context -> params -> (((unit -> string) * stature) * thm) list -> thm
     -> prover_result
@@ -45,8 +41,8 @@
   val learn_proof : theory -> term -> thm list -> unit
 
   val relevant_facts :
-    Proof.context -> params -> string -> int -> relevance_override -> thm list
-    -> term list -> term -> (((unit -> string) * stature) * thm) list
+    Proof.context -> params -> string -> int -> fact_override -> term list
+    -> term -> (((unit -> string) * stature) * thm) list
     -> (((unit -> string) * stature) * thm) list
 end;
 
@@ -80,8 +76,6 @@
 
 (*** Isabelle helpers ***)
 
-val fact_name_of = prefix fact_prefix o ascii_of
-
 fun escape_meta_char c =
   if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
      c = #")" orelse c = #"," then
@@ -255,12 +249,6 @@
 
 fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
 
-fun iter_facts ctxt (params as {provers, ...}) max_relevant goal =
-  let val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 in
-    iterative_relevant_facts ctxt params (hd provers) max_relevant NONE
-                             no_relevance_override [] hyp_ts concl_t
-  end
-
 fun run_prover ctxt (params as {provers, ...}) facts goal =
   let
     val problem =
@@ -325,7 +313,7 @@
       in File.append path s end
   in List.app do_thm ths end
 
-fun generate_atp_dependencies ctxt (params as {max_relevant, ...}) thy
+fun generate_atp_dependencies ctxt (params as {provers, max_relevant, ...}) thy
                               include_thy file_name =
   let
     val path = file_name |> Path.explode
@@ -348,6 +336,7 @@
       let
         val name = Thm.get_name_hint th
         val goal = goal_of_thm thy th
+        val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
         val deps =
           case isabelle_dependencies_of all_names th of
             [] => []
@@ -357,7 +346,8 @@
               val facts =
                 facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
               val facts =
-                facts |> iter_facts ctxt params (the max_relevant) goal
+                facts |> iterative_relevant_facts ctxt params (hd provers)
+                             (the max_relevant) NONE hyp_ts concl_t
                       |> fold (add_isa_dep facts) isa_deps
                       |> map fix_name
             in
@@ -385,12 +375,11 @@
 fun learn_thy thy timeout =
   ()
 
-fun learn_proof thy t thms =
+fun learn_proof thy t ths =
   ()
 
 fun relevant_facts ctxt params prover max_relevant
-                   (override as {add, only, ...}) chained_ths hyp_ts concl_t
-                   facts =
+        ({add, only, ...} : fact_override) hyp_ts concl_t facts =
   if only then
     facts
   else if max_relevant <= 0 then
@@ -398,13 +387,13 @@
   else
     let
       val add_ths = Attrib.eval_thms ctxt add
-      fun prepend_facts ths facts =
+      fun prepend_facts ths accepts =
         ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
-         (facts |> filter_out (member Thm.eq_thm_prop ths o snd)))
+         (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
         |> take max_relevant
     in
-      iterative_relevant_facts ctxt params prover max_relevant NONE override
-                               chained_ths hyp_ts concl_t facts
+      iterative_relevant_facts ctxt params prover max_relevant NONE
+                               hyp_ts concl_t facts
       |> not (null add_ths) ? prepend_facts add_ths
     end
 
diff -r 72129a5c1a8d -r 7fcee834c7f5 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -45,18 +45,14 @@
 
 (** Sledgehammer commands **)
 
-fun add_relevance_override ns : relevance_override =
-  {add = ns, del = [], only = false}
-fun del_relevance_override ns : relevance_override =
-  {add = [], del = ns, only = false}
-fun only_relevance_override ns : relevance_override =
-  {add = ns, del = [], only = true}
-fun merge_relevance_override_pairwise (r1 : relevance_override)
-                                      (r2 : relevance_override) =
+fun add_fact_override ns : fact_override = {add = ns, del = [], only = false}
+fun del_fact_override ns : fact_override = {add = [], del = ns, only = false}
+fun only_fact_override ns : fact_override = {add = ns, del = [], only = true}
+fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) =
   {add = #add r1 @ #add r2, del = #del r1 @ #del r2,
    only = #only r1 andalso #only r2}
-fun merge_relevance_overrides rs =
-  fold merge_relevance_override_pairwise rs (only_relevance_override [])
+fun merge_fact_overrides rs =
+  fold merge_fact_override_pairwise rs (only_fact_override [])
 
 (*** parameters ***)
 
@@ -350,7 +346,7 @@
     (if i = 1 then "" else " " ^ string_of_int i)
   end
 
-fun hammer_away override_params subcommand opt_i relevance_override state =
+fun hammer_away override_params subcommand opt_i fact_override state =
   let
     val ctxt = Proof.context_of state
     val override_params = override_params |> map (normalize_raw_param ctxt)
@@ -358,7 +354,7 @@
     if subcommand = runN then
       let val i = the_default 1 opt_i in
         run_sledgehammer (get_params Normal ctxt override_params) Normal i
-                         relevance_override (minimize_command override_params i)
+                         fact_override (minimize_command override_params i)
                          state
         |> K ()
       end
@@ -366,7 +362,7 @@
       run_minimize (get_params Minimize ctxt
                                (("provers", [default_minimize_prover]) ::
                                 override_params))
-                   (the_default 1 opt_i) (#add relevance_override) state
+                   (the_default 1 opt_i) (#add fact_override) state
     else if subcommand = messagesN then
       messages opt_i
     else if subcommand = supported_proversN then
@@ -381,8 +377,8 @@
       error ("Unknown subcommand: " ^ quote subcommand ^ ".")
   end
 
-fun sledgehammer_trans (((subcommand, params), relevance_override), opt_i) =
-  Toplevel.keep (hammer_away params subcommand opt_i relevance_override
+fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) =
+  Toplevel.keep (hammer_away params subcommand opt_i fact_override
                  o Toplevel.proof_of)
 
 fun string_for_raw_param (name, value) = name ^ " = " ^ implode_param value
@@ -410,19 +406,19 @@
 val parse_fact_refs =
   Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
 val parse_relevance_chunk =
-  (Args.add |-- Args.colon |-- parse_fact_refs >> add_relevance_override)
-  || (Args.del |-- Args.colon |-- parse_fact_refs >> del_relevance_override)
-  || (parse_fact_refs >> only_relevance_override)
-val parse_relevance_override =
+  (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)
+  || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)
+  || (parse_fact_refs >> only_fact_override)
+val parse_fact_override =
   Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
-                              >> merge_relevance_overrides))
-                no_relevance_override
+                              >> merge_fact_overrides))
+                no_fact_override
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "sledgehammer"}
     "search for first-order proof using automatic theorem provers"
     ((Scan.optional Parse.short_ident runN -- parse_params
-      -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
+      -- parse_fact_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
 val _ =
   Outer_Syntax.command @{command_spec "sledgehammer_params"}
     "set and display the default parameters for Sledgehammer"
@@ -434,7 +430,7 @@
     val mode = if auto then Auto_Try else Try
     val i = 1
   in
-    run_sledgehammer (get_params mode ctxt []) mode i no_relevance_override
+    run_sledgehammer (get_params mode ctxt []) mode i no_fact_override
                      (minimize_command [] i) state
   end
 
diff -r 72129a5c1a8d -r 7fcee834c7f5 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -327,7 +327,7 @@
   let
     val ctxt = Proof.context_of state
     val reserved = reserved_isar_keyword_table ()
-    val chained_ths = normalize_chained_theorems (#facts (Proof.goal state))
+    val chained_ths = #facts (Proof.goal state)
     val css_table = clasimpset_rule_table_of ctxt
     val facts =
       refs |> maps (map (apsnd single)
diff -r 72129a5c1a8d -r 7fcee834c7f5 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -9,7 +9,7 @@
 signature SLEDGEHAMMER_RUN =
 sig
   type minimize_command = ATP_Proof_Reconstruct.minimize_command
-  type relevance_override = Sledgehammer_Fact.relevance_override
+  type fact_override = Sledgehammer_Fact.fact_override
   type mode = Sledgehammer_Provers.mode
   type params = Sledgehammer_Provers.params
 
@@ -18,7 +18,7 @@
   val timeoutN : string
   val unknownN : string
   val run_sledgehammer :
-    params -> mode -> int -> relevance_override
+    params -> mode -> int -> fact_override
     -> ((string * string list) list -> string -> minimize_command)
     -> Proof.state -> bool * (string * Proof.state)
 end;
@@ -157,7 +157,7 @@
 
 fun run_sledgehammer (params as {debug, verbose, blocking, provers,
                                  max_relevant, slice, ...})
-        mode i (relevance_override as {only, ...}) minimize_command state =
+        mode i (fact_override as {only, ...}) minimize_command state =
   if null provers then
     error "No prover is set."
   else case subgoal_count state of
@@ -170,12 +170,10 @@
         state |> Proof.map_context (Config.put SMT_Config.verbose debug)
       val ctxt = Proof.context_of state
       val {facts = chained_ths, goal, ...} = Proof.goal state
-      val chained_ths = chained_ths |> normalize_chained_theorems
       val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
       val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
       val facts =
-        nearly_all_facts ctxt ho_atp relevance_override chained_ths hyp_ts
-                         concl_t
+        nearly_all_facts ctxt ho_atp fact_override chained_ths hyp_ts concl_t
       val _ = () |> not blocking ? kill_provers
       val _ = case find_first (not o is_prover_supported ctxt) provers of
                 SOME name => error ("No such prover: " ^ name ^ ".")
@@ -224,7 +222,7 @@
                 SOME is_app => filter (is_app o prop_of o snd)
               | NONE => I)
           |> relevant_facts ctxt params (hd provers) max_max_relevant
-                            relevance_override chained_ths hyp_ts concl_t
+                            fact_override hyp_ts concl_t
           |> map (apfst (apfst (fn name => name ())))
           |> tap (fn facts =>
                      if debug then
diff -r 72129a5c1a8d -r 7fcee834c7f5 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -12,7 +12,6 @@
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time_option : string -> string -> Time.time option
   val subgoal_count : Proof.state -> int
-  val normalize_chained_theorems : thm list -> thm list
   val reserved_isar_keyword_table : unit -> unit Symtab.table
   val thms_in_proof : string list option -> thm -> string list
 end;
@@ -55,11 +54,8 @@
 
 val subgoal_count = Try.subgoal_count
 
-val normalize_chained_theorems =
-  maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
 fun reserved_isar_keyword_table () =
-  Keyword.dest () |-> union (op =)
-  |> map (rpair ()) |> Symtab.make
+  Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make
 
 (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
    fixes that seem to be missing over there; or maybe the two code portions are