optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)

--- a/src/HOL/TPTP/atp_theory_export.ML	Tue Jun 24 14:56:08 2014 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Tue Jun 24 15:08:19 2014 +0200
@@ -155,6 +155,8 @@
 fun heading_sort_key heading =
   if String.isPrefix "Relevant fact" heading then "_" ^ heading else heading
 
+val max_dependencies = 100
+
 fun problem_of_theory ctxt thy format infer_policy type_enc =
   let
     val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
@@ -182,8 +184,8 @@
         facts
         |> map (fn (_, th) =>
                    (fact_name_of (Thm.get_name_hint th),
-                    th |> Sledgehammer_Util.thms_in_proof (SOME name_tabs)
-                       |> map fact_name_of))
+                    th |> Sledgehammer_Util.thms_in_proof max_dependencies (SOME name_tabs)
+                       |> these |> map fact_name_of))
     val all_problem_names =
       problem |> maps (map ident_of_problem_line o snd)
               |> distinct (op =)

--- a/src/HOL/TPTP/mash_eval.ML	Tue Jun 24 14:56:08 2014 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Tue Jun 24 15:08:19 2014 +0200
@@ -111,7 +111,7 @@
             | NONE => error ("No fact called \"" ^ name ^ "\".")
           val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
-          val isar_deps = isar_dependencies_of name_tabs th
+          val isar_deps = these (isar_dependencies_of name_tabs th)
           val facts =
             facts
             |> filter (fn (_, th') =>

--- a/src/HOL/TPTP/mash_export.ML	Tue Jun 24 14:56:08 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Tue Jun 24 15:08:19 2014 +0200
@@ -90,6 +90,7 @@
 
 val prover_marker = "$a"
 val isar_marker = "$i"
+val missing_marker = "$m"
 val omitted_marker = "$o"
 val unprovable_marker = "$u" (* axiom or definition or characteristic theorem *)
 val prover_failed_marker = "$x"
@@ -105,9 +106,14 @@
         let
           val deps =
             (case isar_deps_opt of
-              SOME deps => deps
-            | NONE => isar_dependencies_of name_tabs th)
-        in (if null deps then unprovable_marker else isar_marker, deps) end)
+              NONE => isar_dependencies_of name_tabs th
+            | deps => deps)
+        in
+          ((case deps of
+             NONE => missing_marker
+           | SOME [] => unprovable_marker
+           | SOME deps => isar_marker), [])
+        end)
   in
     (case trim_dependencies deps of
       SOME deps => (marker, deps)
@@ -147,7 +153,7 @@
 fun is_bad_query ctxt ho_atp step j th isar_deps =
   j mod step <> 0 orelse
   Thm.legacy_get_kind th = "" orelse
-  null isar_deps orelse
+  null (the_list isar_deps) orelse
   is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
 
 fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys max_suggs file_name =
@@ -170,7 +176,7 @@
             |> sort_wrt fst
           val access_facts = filter_accessible_from th new_facts @ old_facts
           val (marker, deps) =
-            smart_dependencies_of ctxt params_opt access_facts name_tabs th (SOME isar_deps)
+            smart_dependencies_of ctxt params_opt access_facts name_tabs th isar_deps
 
           fun extra_features_of (((_, stature), th), weight) =
             [prop_of th]

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Jun 24 14:56:08 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Jun 24 15:08:19 2014 +0200
@@ -83,7 +83,7 @@
   val features_of : Proof.context -> theory -> int -> int Symtab.table -> stature -> term list ->
     (string * real) list
   val trim_dependencies : string list -> string list option
-  val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list
+  val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list option
   val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list ->
     string Symtab.table * string Symtab.table -> thm -> bool * string list
   val attach_parents_to_facts : ('a * thm) list -> ('a * thm) list ->
@@ -1153,21 +1153,22 @@
   if length deps > max_dependencies then NONE else SOME deps
 
 fun isar_dependencies_of name_tabs th =
-  let val deps = thms_in_proof (SOME name_tabs) th in
+  thms_in_proof max_dependencies (SOME name_tabs) th
+  |> Option.map (fn deps =>
     if deps = [typedef_dep] orelse deps = [class_some_dep] orelse
        exists (member (op =) fundef_ths) deps orelse exists (member (op =) typedef_ths) deps orelse
        is_size_def deps th then
       []
     else
-      deps
-  end
+      deps)
 
 fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto_level facts
     name_tabs th =
   (case isar_dependencies_of name_tabs th of
-    [] => (false, [])
-  | isar_deps =>
+    SOME [] => (false, [])
+  | isar_deps0 =>
     let
+      val isar_deps = these isar_deps0
       val thy = Proof_Context.theory_of ctxt
       val goal = goal_of_thm thy th
       val name = nickname_of_thm th
@@ -1533,7 +1534,6 @@
             |> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps)
           else
             isar_dependencies_of name_tabs th
-            |> trim_dependencies
 
         fun do_commit [] [] [] state = state
           | do_commit learns relearns flops {access_G, num_known_facts, dirty} =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Jun 24 14:56:08 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Jun 24 15:08:19 2014 +0200
@@ -19,7 +19,8 @@
   val parse_time : string -> string -> Time.time
   val subgoal_count : Proof.state -> int
   val reserved_isar_keyword_table : unit -> unit Symtab.table
-  val thms_in_proof : (string Symtab.table * string Symtab.table) option -> thm -> string list
+  val thms_in_proof : int -> (string Symtab.table * string Symtab.table) option -> thm ->
+    string list option
   val thms_of_name : Proof.context -> string -> thm list
   val one_day : Time.time
   val one_year : Time.time
@@ -84,11 +85,13 @@
 fun reserved_isar_keyword_table () =
   Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make
 
+exception TOO_MANY of unit
+
 (* 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 not doing the same? *)
-fun fold_body_thm outer_name (map_plain_name, map_inclass_name) =
+fun fold_body_thm max_thms outer_name (map_plain_name, map_inclass_name) body =
   let
-    fun app_thm map_name (_, (name, _, body)) accum =
+    fun app_thm map_name (_, (name, _, body)) (accum as (num_thms, names)) =
       let
         val (anonymous, enter_class) =
           (* The "name = outer_name" case caters for the uncommon case where the proved theorem
@@ -98,18 +101,25 @@
           else (false, false)
       in
         if anonymous then
-          accum |> app_body (if enter_class then map_inclass_name else map_name) (Future.join body)
+          app_body (if enter_class then map_inclass_name else map_name) (Future.join body) accum
         else
-          accum |> union (op =) (the_list (map_name name))
+          (case map_name name of
+            SOME name' =>
+            if member (op =) names name' then accum
+            else if num_thms = max_thms then raise TOO_MANY ()
+            else (num_thms + 1, name' :: names)
+          | NONE => accum)
       end
     and app_body map_name (PBody {thms, ...}) = fold (app_thm map_name) thms
   in
-    app_body map_plain_name
+    snd (app_body map_plain_name body (0, []))
   end
 
-fun thms_in_proof name_tabs th =
+fun thms_in_proof max_thms name_tabs th =
   let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in
-    fold_body_thm (Thm.get_name_hint th) map_names (Proofterm.strip_thm (Thm.proof_body_of th)) []
+    SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names
+      (Proofterm.strip_thm (Thm.proof_body_of th)))
+    handle TOO_MANY () => NONE
   end
 
 fun thms_of_name ctxt name =