# HG changeset patch
# User blanchet
# Date 1292702854 -3600
# Node ID 35ce17cd796735282ce8a89c286e61f695808113
# Parent  b806a767808309bb566f683beabab5c7092295fe
made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever);
disabled inductions (E and SPASS don't like them), but kept "ext" (seems more harmless)

diff -r b806a7678083 -r 35ce17cd7967 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Dec 18 18:43:16 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Dec 18 21:07:34 2010 +0100
@@ -53,8 +53,9 @@
 val trace = Unsynchronized.ref false
 fun trace_msg msg = if !trace then tracing (msg ()) else ()
 
-(* experimental feature *)
+(* experimental features *)
 val respect_no_atp = true
+val instantiate_inducts = false
 
 datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
 
@@ -256,8 +257,6 @@
   if (not also_skolem andalso String.isPrefix skolem_prefix s) then I
   else Symtab.map_default (s, [p]) (insert (op =) p)
 
-fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
-
 fun pconsts_in_terms thy is_built_in_const also_skolems pos ts =
   let
     val flip = Option.map not
@@ -286,7 +285,7 @@
           else
             I)
     and do_term_or_formula T =
-      if is_formula_type T then do_formula NONE else do_term
+      if T = HOLogic.boolT then do_formula NONE else do_term
     and do_formula pos t =
       case t of
         Const (@{const_name all}, _) $ Abs (_, T, t') =>
@@ -636,6 +635,7 @@
   ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
    "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
    "weak_case_cong"]
+  |> not instantiate_inducts ? append ["induct", "inducts"]
   |> map (prefix ".")
 
 val max_lambda_nesting = 3
@@ -651,7 +651,7 @@
 fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
     formula_has_too_many_lambdas (T :: Ts) t
   | formula_has_too_many_lambdas Ts t =
-    if is_formula_type (fastype_of1 (Ts, t)) then
+    if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
       exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
     else
       term_has_too_many_lambdas max_lambda_nesting t
@@ -877,7 +877,8 @@
                o fact_from_ref ctxt reserved chained_ths) add
        else
          all_facts ctxt reserved no_dangerous_types fudge add_ths chained_ths)
-      |> maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
+      |> instantiate_inducts
+         ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
       |> rearrange_facts ctxt (respect_no_atp andalso not only)
       |> uniquify
   in