# HG changeset patch
# User blanchet
# Date 1336661783 -7200
# Node ID 67663c968d707dca1097cb24ebc4c759287f222b
# Parent  920ea85e7426da6a905c373c646932acd3e413c8
distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers

diff -r 920ea85e7426 -r 67663c968d70 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu May 10 12:23:20 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu May 10 16:56:23 2012 +0200
@@ -190,10 +190,16 @@
   else if is_assum assms th then Assum
   else Local
 
+val may_be_induction =
+  exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) =>
+                     body_type T = @{typ bool}
+                   | _ => false)
+
 fun status_of_thm css_table name th =
   (* FIXME: use structured name *)
-  if String.isSubstring ".induct" name orelse
-     String.isSubstring ".inducts" name then
+  if (String.isSubstring ".induct" name orelse
+      String.isSubstring ".inducts" name) andalso
+     may_be_induction (prop_of th) then
     Induction
   else case Termtab.lookup css_table (prop_of th) of
     SOME status => status
diff -r 920ea85e7426 -r 67663c968d70 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu May 10 12:23:20 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu May 10 16:56:23 2012 +0200
@@ -172,9 +172,6 @@
   get_prover ctxt mode name params minimize_command problem
   |> minimize ctxt mode name params problem
 
-fun is_induction_fact (Untranslated_Fact ((_, (_, Induction)), _)) = true
-  | is_induction_fact _ = false
-
 fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,
                               timeout, expect, ...})
         mode minimize_command only {state, goal, subgoal, subgoal_count, facts}
@@ -191,14 +188,13 @@
     fun desc () =
       prover_description ctxt params name num_facts subgoal subgoal_count goal
     val problem =
-      let
-        val filter_induction = filter_out is_induction_fact
-      in {state = state, goal = goal, subgoal = subgoal,
-         subgoal_count = subgoal_count, facts =
-          ((Sledgehammer_Provers.is_ho_atp ctxt name |> not) ? filter_induction)
-            facts
-          |> take num_facts}
-      end
+      {state = state, goal = goal, subgoal = subgoal,
+       subgoal_count = subgoal_count,
+       facts = facts
+               |> not (Sledgehammer_Provers.is_ho_atp ctxt name)
+                  ? filter_out (curry (op =) Induction o snd o snd o fst
+                                o untranslated_fact)
+               |> take num_facts}
     fun really_go () =
       problem
       |> get_minimizing_prover ctxt mode name params minimize_command