# HG changeset patch
# User blanchet
# Date 1341956163 -7200
# Node ID d7ad89f6076824a3bbd71ac91b6eb2e9f1b4ae74
# Parent  e174ecc4f5a445042f27ac16ee81976fbc64b72c
export useful functions

diff -r e174ecc4f5a4 -r d7ad89f60768 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Jul 10 23:36:03 2012 +0200
@@ -53,6 +53,10 @@
     Proof.context -> bool -> 'a Symtab.table -> bool -> thm list
     -> thm list -> status Termtab.table
     -> (((unit -> string) * stature) * thm) list
+  val maybe_instantiate_inducts :
+    Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
+    -> (((unit -> string) * 'a) * thm) list
+  val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
   val nearly_all_facts :
     Proof.context -> bool -> relevance_override -> thm list -> term list -> term
     -> (((unit -> string) * stature) * thm) list
@@ -959,19 +963,29 @@
 fun external_frees t =
   [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
 
+fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
+  if Config.get ctxt instantiate_inducts then
+    let
+      val thy = Proof_Context.theory_of ctxt
+      val ind_stmt =
+        (hyp_ts |> filter_out (null o external_frees), concl_t)
+        |> Logic.list_implies |> Object_Logic.atomize_term thy
+      val ind_stmt_xs = external_frees ind_stmt
+    in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end
+  else
+    I
+
+fun maybe_filter_no_atps ctxt =
+  not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
+
 fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override)
                      chained_ths hyp_ts concl_t =
   if only andalso null add then
     []
   else
     let
-      val thy = Proof_Context.theory_of ctxt
       val reserved = reserved_isar_keyword_table ()
       val add_ths = Attrib.eval_thms ctxt add
-      val ind_stmt =
-        (hyp_ts |> filter_out (null o external_frees), concl_t)
-        |> Logic.list_implies |> Object_Logic.atomize_term thy
-      val ind_stmt_xs = external_frees ind_stmt
       val css_table = clasimpset_rule_table_of ctxt
     in
       (if only then
@@ -979,10 +993,8 @@
                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)
-      |> Config.get ctxt instantiate_inducts
-         ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
-      |> (not (Config.get ctxt ignore_no_atp) andalso not only)
-         ? filter_out (No_ATPs.member ctxt o snd)
+      |> maybe_instantiate_inducts ctxt hyp_ts concl_t
+      |> not only ? maybe_filter_no_atps ctxt
       |> uniquify
     end